Theory Ground_Terms

theory Ground_Terms
  imports TRS.Term_More
begin

lemma [simp]:
  "i < length xs ⟹ Suc (length xs - Suc 0) = length xs" by auto

subsection ‹Equality on ground terms by positions and symbols›

fun fun_at :: "('f, 'v) term ⇒ pos ⇒ 'f option" where
  "fun_at (Var x) p = None"
| "fun_at (Fun f ts) [] = Some f"
| "fun_at (Fun f ts) (i # p) = (if i < length ts then fun_at (ts ! i) p else None)"

lemma fun_at_def':
  "fun_at t p = (if p ∈ poss t then map_option fst (root (t |_ p)) else None)"
  by (induct t p rule: fun_at.induct) auto

lemma eq_term_by_poss_fun_at:
  assumes "poss s = poss t" "ground s" "⋀p. p ∈ poss s ⟹ fun_at s p = fun_at t p"
  shows "s = t"
  using assms
proof (induct s arbitrary: t)
  case (Fun f ss) note Fun' = this
  show ?case
  proof (cases t)
    case (Var x) show ?thesis using Fun'(4)[of "[]"] by (simp add: Var)
  next
    case (Fun g ts)
    have *: "length ss = length ts"
      using Fun'(3) arg_cong[OF Fun'(2), of "λP. card {i |i p. i # p ∈ P}"]
      by (auto simp: Fun exI[of "λx. x ∈ poss _", OF empty_pos_in_poss])
    then have "i < length ss ⟹ poss (ss ! i) = poss (ts ! i)" for i
      using arg_cong[OF Fun'(2), of "λP. {p. i # p ∈ P}"] by (auto simp: Fun)
    then show ?thesis using * Fun'(3) Fun'(4)[of "[]"] Fun'(4)[of "_ # _ :: pos"]
      by (auto simp: Fun intro!: nth_equalityI Fun'(1)[OF nth_mem, of n "ts ! n" for n])
  qed
qed simp


subsection ‹Ground terms›

text ‹This type serves two purposes. First of all, the encoding definitions and proofs are not
littered by cases for variables. Secondly, we can consider tree domains (usually sets of positions),
so they become a special case of ground terms. This enables the construction of a term from a
tree domain and a function from positions to symbols.›

datatype 'f gterm =
  GFun (groot: 'f) (gargs: "'f gterm list")

fun term_of_gterm where
  "term_of_gterm (GFun f ts) = Fun f (map term_of_gterm ts)"

fun gterm_of_term where
  "gterm_of_term (Fun f ts) = GFun f (map gterm_of_term ts)"

lemma length_args_length_gargs [simp]:
  "length (args (term_of_gterm t)) = length (gargs t)"
  by (cases t) auto

lemma ground_term_of_gterm [simp]:
  "ground (term_of_gterm s)"
  by (induct s) auto

lemma term_of_gterm_inv [simp]:
  "gterm_of_term (term_of_gterm t) = t"
  by (induct t) (auto intro!: nth_equalityI)

lemma inj_term_of_gterm:
  "inj_on term_of_gterm X"
  by (metis inj_on_def term_of_gterm_inv)

lemma gterm_of_term_inv [simp]:
  "ground t ⟹ term_of_gterm (gterm_of_term t) = t"
  by (induct t) (auto 0 0 intro!: nth_equalityI)

lemma ground_term_to_gtermD:
  "ground t ⟹ ∃t'. t = term_of_gterm t'"
  by (metis gterm_of_term_inv)

lemma map_term_of_gterm [simp]:
  "map_term f g (term_of_gterm t) = term_of_gterm (map_gterm f t)"
  by (induct t) auto

lemma map_gterm_of_term [simp]:
  "ground t ⟹ gterm_of_term (map_term f g t) = map_gterm f (gterm_of_term t)"
  by (induct t) auto

lemma gterm_set_gterm_funs_terms:
  "set_gterm t = funs_term (term_of_gterm t)"
  by (induct t) auto

lemma term_set_gterm_funs_terms:
  assumes "ground t"
  shows "set_gterm (gterm_of_term t) = funs_term t"
  using assms by (induct t) auto

abbreviation gctxt_apply where
  "gctxt_apply C t ≡ gterm_of_term C⟨term_of_gterm t :: (_, unit) term⟩"

abbreviation gposs where
  "gposs ≡ λt. poss (term_of_gterm t :: (_, unit) term)"

lemma gposs_map_gterm [simp]:
  "gposs (map_gterm f s) = gposs s"
  by (induct s) auto

lemma poss_gposs_conv:
  "gposs t = poss (term_of_gterm t)"
  by (induct t) auto

abbreviation gfun_at where
  "gfun_at t p ≡ fun_at (term_of_gterm t :: (_, unit) term) p"

lemma gfun_at_map_gterm [simp]:
  "gfun_at (map_gterm f t) p = map_option f (gfun_at t p)"
  by (induct t arbitrary: p; case_tac p) (auto simp: comp_def)

lemma set_gterm_gposs_conv:
  "set_gterm t = {the (gfun_at t p) |p. p ∈ gposs t}"
proof (induct t)
  case (GFun f ts)
  have [simp]: "{the (fun_at (Fun f (map term_of_gterm ts :: (_, unit) term list)) p) |p.
    ∃i pa. p = i # pa ∧ i < length ts ∧ pa ∈ gposs (ts ! i)} =
    (⋃x∈{ts ! i |i. i < length ts}. {the (gfun_at x p) |p. p ∈ gposs x})" (* eww *)
    unfolding UNION_eq
  proof ((intro set_eqI iffI; elim CollectE exE bexE conjE), goal_cases lr rl)
    case (lr x p i pa) then show ?case
      by (intro CollectI[of _ x] bexI[of _ "ts ! i"] exI[of _ pa]) auto
  next
    case (rl x xa i p) then show ?case
      by (intro CollectI[of _ x] exI[of _ "i # p"]) auto
  qed
  show ?case
    by (simp add: GFun(1) set_conv_nth conj_disj_distribL ex_disj_distrib Collect_disj_eq cong: conj_cong)
qed

text ‹A @{type gterm} version of lemma @{verbatim eq_term_by_poss_fun_at}.›

lemmas eq_gterm_by_gposs_gfun_at = arg_cong[where f = gterm_of_term,
  OF eq_term_by_poss_fun_at[OF _ ground_term_of_gterm, of _ "term_of_gterm t :: (_, unit) term" for t],
  unfolded term_of_gterm_inv]

fun gsubt_at :: "'f gterm ⇒ pos ⇒ 'f gterm" where
  "gsubt_at s [] = s" |
  "gsubt_at (GFun f ss) (i # p) = gsubt_at (ss ! i) p"

lemma gsubt_at_to_subt_at [simp]:
  assumes "p ∈ gposs s"
  shows "gsubt_at s p = gterm_of_term (term_of_gterm s |_ p)"
  using assms by (induct arbitrary: p) (auto simp add: map_idI) 

lemma gsubt_at_to_ctxt:
  assumes "p ∈ gposs s"
  shows "∃ C u. gsubt_at s p = u ∧ gterm_of_term C⟨term_of_gterm u⟩ = s"
  using assms
  by (induct s arbitrary: p) (metis ctxt_supt_id ground_ctxt_apply ground_term_of_gterm gsubt_at_to_subt_at gterm_of_term_inv poss_gposs_conv term_of_gterm_inv)

lemma gsubt_at_gposs [simp]:
  assumes "p ∈ gposs s"
  shows "gposs (gsubt_at s p) = {x | x. p @ x ∈ gposs s}"
  using assms by (induct s arbitrary: p) auto

lemma gfun_at_gsub_at [simp]:
  assumes "p ∈ gposs s" and "p @ q ∈ gposs s"
  shows "gfun_at (gsubt_at s p) q = gfun_at s (p @ q)"
  using assms by (induct s arbitrary: p q) auto

lemma gposs_gsubst_at_subst_at_eq [simp]:
  assumes "p ∈ gposs s"
  shows "gposs (gsubt_at s p) = poss (term_of_gterm s |_ p)" using assms
proof (induct s arbitrary: p)
  case (GFun f ts)
  show ?case using GFun(1)[OF nth_mem] GFun(2-) apply auto
    using empty_pos_in_poss by fastforce+
qed

lemma gpos_append_gposs:
  assumes "p ∈ gposs t" and "q ∈ gposs (gsubt_at t p)"
  shows "p @ q ∈ gposs t"
  using assms by auto

lemma ctxt_of_pos_gterm_gsubt_at_to_gterm:
  assumes "p ∈ gposs t"
  shows "gterm_of_term (ctxt_of_pos_term p (term_of_gterm t))⟨term_of_gterm (gsubt_at t p)⟩ = t"
  using assms by (induct t arbitrary: p) (auto simp: comp_def min_def nth_append_Cons intro!: nth_equalityI)  


subsection ‹Tree domains›

type_synonym gdomain = "unit gterm"

abbreviation gdomain where
  "gdomain ≡ map_gterm (λ_. ())"

lemma gdomain_id:
  "gdomain t = t"
proof -
  have [simp]: "(λ_. ()) = id" by auto
  then show ?thesis by (simp add: gterm.map_id)
qed

lemma gdomain_gsubt [simp]:
  assumes "p ∈ gposs t"
  shows "gdomain (gsubt_at t p) = gsubt_at (gdomain t) p"
  using assms by (induct t arbitrary: p) auto

text ‹Union of tree domains›

fun gunion :: "gdomain ⇒ gdomain ⇒ gdomain" where
  "gunion (GFun f ss) (GFun g ts) = GFun () (map (λi.
    if i < length ss then if i < length ts then gunion (ss ! i) (ts ! i)
    else ss ! i else ts ! i) [0..<max (length ss) (length ts)])"

lemma gposs_gunion [simp]:
  "gposs (gunion s t) = gposs s ∪ gposs t"
  by (induct s t rule: gunion.induct) (auto simp: less_max_iff_disj split: if_splits)

lemma gunion_unit [simp]:
  "gunion s (GFun () []) = s" "gunion (GFun () []) s = s"
  by (cases s, (auto intro!: nth_equalityI)[1])+

lemma gunion_gsubt_at_nt_poss1:
  assumes "p ∈ gposs s" and "p ∉ gposs t"
  shows "gsubt_at (gunion s t) p = gsubt_at s p"
  using assms by (induct s arbitrary: p t) (case_tac p; case_tac t, auto)


lemma gunion_gsubt_at_nt_poss2:
  assumes "p ∈ gposs t" and "p ∉ gposs s"
  shows "gsubt_at (gunion s t) p = gsubt_at t p"
  using assms by (induct t arbitrary: p s) (case_tac p; case_tac s, auto)


lemma gunion_gsubt_at_poss:
  assumes "p ∈ gposs s" and "p ∈ gposs t"
  shows "gunion (gsubt_at s p) (gsubt_at t p) = gsubt_at (gunion s t) p"
  using assms
proof (induct p arbitrary: s t)
  case (Cons a p)
  then show ?case by (cases s; cases t) auto 
qed auto 

lemma gfun_at_domain:
  shows "gfun_at t p = (if p ∈ gposs t then Some () else None)"
proof -
  define t' where "t' ≡ term_of_gterm t :: (_, unit) term"
  have "ground t'" by (simp add: t'_def ground_term_of_gterm)
  then show ?thesis unfolding t'_def[symmetric]
    by (induct t' arbitrary: p; case_tac p) auto
qed

lemma gunion_assoc [ac_simps]:
  "gunion s (gunion t u) = gunion (gunion s t) u"
  by (intro eq_gterm_by_gposs_gfun_at) (auto simp: gfun_at_domain)

lemma gunion_commute [ac_simps]:
  "gunion s t = gunion t s"
  by (intro eq_gterm_by_gposs_gfun_at) (auto simp: gfun_at_domain)

lemma gunion_idemp [simp]:
  "gunion s s = s"
  by (intro eq_gterm_by_gposs_gfun_at) (auto simp: gfun_at_domain)

definition gunions :: "gdomain list ⇒ gdomain" where
  "gunions ts = foldr gunion ts (GFun () [])"

lemma gunions_append:
  "gunions (ss @ ts) = gunion (gunions ss) (gunions ts)"
  by (induct ss) (auto simp: gunions_def gunion_assoc)

lemma gposs_gunions [simp]:
  "gposs (gunions ts) = {[]} ∪ ⋃{gposs t |t. t ∈ set ts}"
  by (induct ts) (auto simp: gunions_def)


text ‹Given a tree domain and a function from positions to symbols, we can construct a term.›

fun glabel :: "(pos ⇒ 'f) ⇒ gdomain ⇒ 'f gterm" where
  "glabel h (GFun f ts) = GFun (h []) (map (λi. glabel (h ∘ (#) i) (ts ! i)) [0..<length ts])"

lemma map_gterm_glabel:
  "map_gterm f (glabel h t) = glabel (f ∘ h) t"
  by (induct t arbitrary: h) (auto simp: comp_def)

lemma gfun_at_glabel [simp]:
  "gfun_at (glabel f t) p = (if p ∈ gposs t then Some (f p) else None)"
  by (induct t arbitrary: f p, case_tac p) (auto simp: comp_def)

lemma gposs_glabel [simp]:
  "gposs (glabel f t) = gposs t"
  by (induct t arbitrary: f) auto

lemma glabel_map_gterm_conv:
  "glabel (f ∘ gfun_at t) (gdomain t) = map_gterm (f ∘ Some) t"
  by (induct t) (auto simp: comp_def intro!: nth_equalityI)

lemma gfun_at_nongposs [simp]:
  "p ∉ gposs t ⟹ gfun_at t p = None"
  using gfun_at_glabel[of "the ∘ gfun_at t" "gdomain t" p, unfolded glabel_map_gterm_conv]
  by (simp add: comp_def option.map_ident)

lemma gfun_at_poss:
  "p ∈ gposs t ⟹ ∃f. gfun_at t p = Some f"
  using gfun_at_glabel[of "the ∘ gfun_at t" "gdomain t" p, unfolded glabel_map_gterm_conv]
  by (auto simp: comp_def)

lemma gfun_at_possE:
  assumes "p ∈ gposs t"
  obtains f where "gfun_at t p = Some f"
  using assms gfun_at_poss by blast

text ‹function symbols of a ground term›

definition funas_gterm where
  "funas_gterm s = funas_term (term_of_gterm s :: (_, unit) term)"

lemma funas_gterm_gterm_of_term:
  "ground t ⟹ funas_gterm (gterm_of_term t) = funas_term t"
  by (induct t) (auto simp: funas_gterm_def)

lemma funas_term_of_gterm_conv:
  "funas_term (term_of_gterm t) = funas_gterm t"
  by (induct t) (auto simp: funas_gterm_def)

lemma funas_gterm_map_gterm:
  assumes "funas_gterm t ⊆ ℱ"
  shows "funas_gterm (map_gterm f t) ⊆ (λ (h, n). (f h, n)) ` ℱ"
  using assms by (induct t) (auto simp: funas_gterm_def)

lemma gterm_of_term_inj:
  assumes "⋀ t. t ∈ S ⟹ ground t"
  shows "inj_on gterm_of_term S"
  using assms gterm_of_term_inv by (fastforce simp: inj_on_def)


end