Theory Ground_Terms

theory Ground_Terms
  imports QTRS.Term_More
begin

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.›

"'f gterm list"">datatype 'f gterm = GFun (groot: 'f) "'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 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 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

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

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]


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

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 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 ∘ op <# 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)

end