# Theory Regular_Tree_Relations.Ground_Terms

subsection ‹Ground constructions›

theory Ground_Terms
imports Basic_Utils
begin

subsubsection ‹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),
which 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_sym: 'f) (gargs: "'f gterm list")

lemma gterm_idx_induct[case_names GFun]:
assumes " f ts. ( i. i < length ts  P (ts ! i))  P (GFun f ts)"
shows "P t" using assms
by (induct t) auto

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)"

fun groot where
"groot (GFun f ts) = (f, length ts)"

lemma groot_sym_groot_conv:
"groot_sym t = fst (groot t)"
by (cases t) auto

lemma groot_sym_gterm_of_term:
"ground t  groot_sym (gterm_of_term t) = fst (the (root t))"
by (cases t) auto

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 ground_term_of_gterm' [simp]:
"term_of_gterm s = Fun f ss  ground (Fun f ss)"
by (induct s) auto

lemma term_of_gterm_inv [simp]:

by (induct t) (auto intro!: nth_equalityI)

lemma inj_term_of_gterm:

by (metis inj_on_def term_of_gterm_inv)

lemma gterm_of_term_inv [simp]:

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:

by (induct t) auto

lemma term_set_gterm_funs_terms:
assumes "ground t"
shows
using assms by (induct t) auto

lemma vars_term_of_gterm [simp]:

by (induct t) auto

lemma vars_term_of_gterm_subseteq [simp]:

by auto

context
notes conj_cong [fundef_cong]
begin
fun gposs :: "'f gterm  pos set" where
"gposs (GFun f ss) = {[]}  {i # p | i p. i < length ss  p  gposs (ss ! i)}"
end

lemma gposs_Nil [simp]: "[]  gposs s"
by (cases s) auto

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

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

lemma poss_gposs_mem_conv:
"p  poss (term_of_gterm t)  p  gposs t"
using poss_gposs_conv by auto

lemma gposs_to_poss:
"p  gposs t  p  poss (term_of_gterm t)"

fun gfun_at :: "'f gterm  pos  'f option" where
"gfun_at (GFun f ts) [] = Some f"
| "gfun_at (GFun f ts) (i # p) = (if i < length ts then gfun_at (ts ! i) p else None)"

abbreviation "exInl  case_sum (λ x. x) (λ _.undefined)"

lemma gfun_at_gterm_of_term [simp]:
"ground s  map_option exInl (fun_at s p) = gfun_at (gterm_of_term s) p"
proof (induct p arbitrary: s)
case Nil then show ?case
by (cases s) auto
next
case (Cons i p) then show ?case
by (cases s) auto
qed

lemmas gfun_at_gterm_of_term' [simp] = gfun_at_gterm_of_term[OF ground_term_of_gterm, unfolded term_of_gterm_inv]

lemma gfun_at_None_ngposs_iff: "gfun_at s p = None  p  gposs s"
by (induct rule: gfun_at.induct) auto

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)
note [simp] = gfun_at_gterm_of_term[OF ground_term_of_gterm, unfolded term_of_gterm_inv]
have [simp]: "{the (map_option exInl (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 intro!: arg_cong[where ?f = the])
next
case (rl x xa i p) then show ?case
by (intro CollectI[of _ x] exI[of _ "i  p"]) auto
qed
have [simp]: "(x{ts ! i |i. i < length ts}. {the (gfun_at x p) |p. p  gposs x}) =
{the (gfun_at (GFun f ts) p) |p. i pa. p = i # pa  i < length ts  pa  gposs (ts ! i)}"
by auto (metis gfun_at.simps(2))+
show ?case
by (simp add: GFun(1) set_conv_nth conj_disj_distribL ex_disj_distrib Collect_disj_eq)
qed

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

lemma fun_at_gfun_at_conv:
"fun_at (term_of_gterm s) p = fun_at (term_of_gterm t) p  gfun_at s p = gfun_at t p"
proof (induct p arbitrary: s t)
case Nil then show ?case
by (cases s; cases t) auto
next
case (Cons i p)
obtain f h ss ts where [simp]: "s = GFun f ss" "t = GFun h ts" by (cases s; cases t) auto
have [simp]: "None = fun_at (term_of_gterm (ts ! i)) p  p  gposs (ts ! i)"
using fun_at_None_nposs_iff by (metis poss_gposs_mem_conv)
have [simp]:"None = gfun_at (ts ! i) p  p  gposs (ts ! i)"
using gfun_at_None_ngposs_iff by force
show ?case using Cons[of "gargs s ! i" "gargs t ! i"]
by (auto simp: poss_gposs_conv gfun_at_None_ngposs_iff fun_at_None_nposs_iff
intro!: iffD2[OF gfun_at_None_ngposs_iff] iffD2[OF fun_at_None_nposs_iff])
qed

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

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:
assumes "p  gposs s"
shows
using assms by (induct arbitrary: p) (auto simp add: map_idI)

lemma term_of_gterm_gsubt:
assumes "p  gposs s"
shows "(term_of_gterm s) |_ p = term_of_gterm (gsubt_at s p)"
using assms by (induct arbitrary: p) auto

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-)
by (auto simp: poss_gposs_mem_conv) blast+
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

text ‹Replace terms at position›

fun replace_gterm_at ("_[_  _]G" [1000, 0, 0] 1000) where
"replace_gterm_at s [] t = t"
| "replace_gterm_at (GFun f ts) (i # ps) t =
(if i < length ts then GFun f (ts[i:=(replace_gterm_at (ts ! i) ps t)]) else GFun f ts)"

lemma replace_gterm_at_not_poss [simp]:
"p  gposs s  s[p  t]G = s"
proof (induct s arbitrary: p)
case (GFun f ts) show ?case using GFun(1)[OF nth_mem] GFun(2)
by (cases p) (auto simp: min_def intro!: nth_equalityI)
qed

lemma parallel_replace_gterm_commute [ac_simps]:
"p  q  s[p  t]G[q  u]G = s[q  u]G[p  t]G"
proof (induct s arbitrary: p q)
case (GFun f ts)
from GFun(2) have "p  []" "q  []" by auto
then obtain i j ps qs where [simp]: "p = i # ps" "q = j # qs"
by (cases p; cases q) auto
have "i  j  (GFun f ts)[p  t]G[q  u]G = (GFun f ts)[q  u]G[p  t]G"
by (auto simp: list_update_swap)
then show ?case using GFun(1)[OF nth_mem, of j ps qs] GFun(2)
by (cases "i = j") (auto simp: par_Cons_iff)
qed

lemma replace_gterm_at_above [simp]:
"p p q  s[q  t]G[p  u]G = s[p  u]G"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "gargs s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto

lemma replace_gterm_at_below [simp]:
"p <p q  s[p  t]G[q  u]G = s[p  t[q -p p  u]G]G"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "gargs s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto

lemma groot_sym_replace_gterm [simp]:
"p  []  groot_sym s[p  t]G = groot_sym s"
by (cases s; cases p) auto

lemma replace_gterm_gsubt_at_id [simp]: "s[p  gsubt_at s p]G = s"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) auto
qed auto

lemma replace_gterm_conv:
"p  gposs s  (term_of_gterm s)[p  (term_of_gterm t)] = term_of_gterm (s[p  t]G)"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) (auto simp: nth_list_update intro: nth_equalityI)
qed auto

subsubsection ‹Tree domains›

type_synonym gdomain =

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 ::  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
proof (induct t arbitrary: p)
case (GFun f ts) then show ?case
by (cases 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 poss_gposs_mem_conv)

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

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

definition gunions ::  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.›
context
notes conj_cong [fundef_cong]
begin
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])"
end

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]

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

lemma gfun_at_poss_gpossD:
"gfun_at t p = Some f  p  gposs t"
by (metis gfun_at_nongposs option.distinct(1))

text ‹function symbols of a ground term›

primrec funas_gterm :: "'f gterm  ('f × nat) set" where
"funas_gterm (GFun f ts) = {(f, length ts)}  (set (map funas_gterm ts))"

lemma funas_gterm_gterm_of_term:

by (induct t) (auto simp: funas_gterm_def)

lemma funas_term_of_gterm_conv:

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
using assms gterm_of_term_inv by (fastforce simp: inj_on_def)

lemma funas_gterm_gsubt_at_subseteq:
assumes "p  gposs s"
shows  using assms
apply (induct s arbitrary: p) apply auto
using nth_mem by blast+

lemma finite_funas_gterm: "finite (funas_gterm t)"
by (induct t) auto

text ‹ground term set›

abbreviation gterms where
"gterms   {s. funas_gterm s  }"

lemma gterms_mono:
"𝒢    gterms 𝒢  gterms "
by auto

inductive_set 𝒯G for  where
const [simp]: "(a, 0)    GFun a []  𝒯G "
| ind [intro]: "(f, n)    length ss = n  ( i. i < length ss  ss ! i  𝒯G )  GFun f ss  𝒯G "

lemma 𝒯G_sound:
"s  𝒯G   funas_gterm s  "
proof (induct)
case (GFun f ts)
show ?case using GFun(1)[OF nth_mem] GFun(2)
by (fastforce simp: in_set_conv_nth elim!: 𝒯G.cases intro: nth_mem)
qed

lemma 𝒯G_complete:
"funas_gterm s    s  𝒯G  "
by (induct s) (auto simp: SUP_le_iff)

lemma 𝒯G_funas_gterm_conv:
"s  𝒯G   funas_gterm s  "
using 𝒯G_sound 𝒯G_complete by auto

lemma 𝒯G_equivalent_def:
"𝒯G  = gterms "
using 𝒯G_funas_gterm_conv by auto

lemma 𝒯G_intersection [simp]:
"s  𝒯G   s  𝒯G 𝒢  s  𝒯G (  𝒢)"
by (auto simp: 𝒯G_funas_gterm_conv 𝒯G_equivalent_def)

lemma 𝒯G_mono:
"𝒢    𝒯G 𝒢  𝒯G "
using gterms_mono by (simp add: 𝒯G_equivalent_def)

lemma 𝒯G_UNIV [simp]: "s  𝒯G UNIV"
by (induct) auto

definition funas_grel where
"funas_grel  =  ((λ (s, t). funas_gterm s  funas_gterm t) ` )"

end