dy>

# Theory Term_Context

section â¹Preliminariesâº

theory Term_Context
imports First_Order_Terms.Term
Knuth_Bendix_Order.Subterm_and_Context
Polynomial_Factorization.Missing_List
begin

subsection â¹Additional functionality on @{type term} and @{type ctxt}âº
subsubsection â¹Positionsâº

type_synonym pos = "nat list"
context
notes conj_cong [fundef_cong]
begin

fun poss :: "('f, 'v) term â pos set" where
"poss (Var x) = {[]}"
| "poss (Fun f ss) = {[]} âª {i # p | i p. i < length ss â§ p â poss (ss ! i)}"
end

fun hole_pos where
"hole_pos â¡ = []"
| "hole_pos (More f ss D ts) = length ss # hole_pos D"

definition position_less_eq (infixl "â¤â©p" 67) where
"p â¤â©p q â· (â r. p @ r = q)"

abbreviation position_less (infixl "<â©p" 67) where
"p <â©p q â¡ p â  q â§ p â¤â©p q"

definition position_par  (infixl "â¥" 67) where
"p â¥ q â· Â¬ (p â¤â©p q) â§ Â¬ (q â¤â©p p)"

fun remove_prefix where
"remove_prefix (x # xs) (y # ys) = (if x = y then remove_prefix xs ys else None)"
| "remove_prefix [] ys = Some ys"
| "remove_prefix xs [] = None"

definition pos_diff  (infixl "-â©p" 67) where
"p -â©p q = the (remove_prefix q p)"

fun subt_at :: "('f, 'v) term â pos â ('f, 'v) term" (infixl "|'_" 67) where
"s |_ [] = s"
| "Fun f ss |_ (i # p) = (ss ! i) |_ p"
| "Var x |_ _ = undefined"

fun ctxt_at_pos where
"ctxt_at_pos s [] = â¡"
| "ctxt_at_pos (Fun f ss) (i # p) = More f (take i ss) (ctxt_at_pos (ss ! i) p) (drop (Suc i) ss)"
| "ctxt_at_pos (Var x) _ = undefined"

fun replace_term_at ("_[_ â _]" [1000, 0, 0] 1000) where
"replace_term_at s [] t = t"
| "replace_term_at (Var x) ps t = (Var x)"
| "replace_term_at (Fun f ts) (i # ps) t =
(if i < length ts then Fun f (ts[i:=(replace_term_at (ts ! i) ps t)]) else Fun f ts)"

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

subsubsection â¹Computing the signatureâº

fun funas_term where
"funas_term (Var x) = {}"
| "funas_term (Fun f ts) = insert (f, length ts) (â (set (map funas_term ts)))"

fun funas_ctxt where
"funas_ctxt â¡ = {}"
| "funas_ctxt (More f ss C ts) = (â (set (map funas_term ss))) âª
insert (f, Suc (length ss + length ts)) (funas_ctxt C) âª (â (set (map funas_term ts)))"

subsubsection â¹Groundnessâº

fun ground where
"ground (Var x) = False"
| "ground (Fun f ts) = (â t â set ts. ground t)"

fun ground_ctxt where
"ground_ctxt â¡ â· True"
| "ground_ctxt (More f ss C ts) â· (â t â set ss. ground t) â§ ground_ctxt C â§ (â t â set ts. ground t)"

subsubsection â¹Depthâº
fun depth where
"depth (Var x) = 0"
| "depth (Fun f []) = 0"
| "depth (Fun f ts) = Suc (Max (depth  set ts))"

subsubsection â¹Type conversionâº

text â¹We require a function which adapts the type of variables of a term,
so that states of the automaton and variables in the term language can be
chosen independently.âº

abbreviation "map_vars_term f â¡ map_term (Î» x. x) f"
abbreviation "map_funs_term f â¡ map_term f (Î» x. x)"
abbreviation "map_both f â¡ map_prod f f"

definition adapt_vars :: "('f, 'q) term â ('f,'v)term" where
[code del]: "adapt_vars â¡ map_vars_term (Î»_. undefined)"

abbreviation "map_vars_ctxt f â¡ map_ctxt (Î»x. x) f"
definition adapt_vars_ctxt :: "('f,'q)ctxt â ('f,'v)ctxt" where
[code del]: "adapt_vars_ctxt = map_vars_ctxt (Î»_. undefined)"

subsection â¹Properties of @{type pos}âº

lemma position_less_eq_induct [consumes 1]:
assumes "p â¤â©p q" and "â p. P p p"
and "â p q r. p â¤â©p q â¹ P p q â¹ P p (q @ r)"
shows "P p q" using assms
proof (induct p arbitrary: q)
case Nil then show ?case
by (metis append_Nil position_less_eq_def)
next
case (Cons a p)
then show ?case
by (metis append_Nil2 position_less_eq_def)
qed

text â¹We show the correspondence between the function @{const remove_prefix} and
the order on positions @{const position_less_eq}. Moreover how it can be used to
compute the difference of positions.âº

lemma remove_prefix_Nil [simp]:
"remove_prefix xs xs = Some []"
by (induct xs) auto

lemma remove_prefix_Some:
assumes "remove_prefix xs ys = Some zs"
shows "ys = xs @ zs" using assms
proof (induct xs arbitrary: ys)
case (Cons x xs)
show ?case using Cons(1)[of "tl ys"] Cons(2)
by (cases ys) (auto split: if_splits)
qed auto

lemma remove_prefix_append:
"remove_prefix xs (xs @ ys) = Some ys"
by (induct xs) auto

lemma remove_prefix_iff:
"remove_prefix xs ys = Some zs â· ys = xs @ zs"
using remove_prefix_Some remove_prefix_append
by blast

lemma position_less_eq_remove_prefix:
"p â¤â©p q â¹ remove_prefix p q â  None"
by (induct rule: position_less_eq_induct) (auto simp: remove_prefix_iff)

text â¹Simplification rules on @{const position_less_eq}, @{const pos_diff},
and @{const position_par}.âº

lemma position_less_refl [simp]: "p â¤â©p p"
by (auto simp: position_less_eq_def)

lemma position_less_eq_Cons [simp]:
"(i # ps) â¤â©p (j # qs) â· i = j â§ ps â¤â©p qs"
by (auto simp: position_less_eq_def)

lemma position_less_Nil_is_bot [simp]: "[] â¤â©p p"
by (auto simp: position_less_eq_def)

lemma position_less_Nil_is_bot2 [simp]: "p â¤â©p [] â· p = []"
by (auto simp: position_less_eq_def)

lemma position_diff_Nil [simp]: "q -â©p [] = q"
by (auto simp: pos_diff_def)

lemma position_diff_Cons [simp]:
"(i # ps) -â©p (i # qs) = ps -â©p qs"
by (auto simp: pos_diff_def)

lemma Nil_not_par [simp]:
"[] â¥ p â· False"
"p â¥ [] â· False"
by (auto simp: position_par_def)

lemma par_not_refl [simp]: "p â¥ p â· False"
by (auto simp: position_par_def)

lemma par_Cons_iff:
"(i # ps) â¥ (j # qs) â· (i â  j â¨ ps â¥ qs)"
by (auto simp: position_par_def)

text â¹Simplification rules on @{const poss}.âº

lemma Nil_in_poss [simp]: "[] â poss t"
by (cases t) auto

lemma poss_Cons [simp]:
"i # p â poss t â¹ [i] â poss t"
by (cases t) auto

lemma poss_Cons_poss:
"i # q â poss t â· i < length (args t) â§ q â poss (args t ! i)"
by (cases t) auto

lemma poss_append_poss:
"p @ q â poss t â· p â poss t â§ q â poss (t |_ p)"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons[of "args t ! i"] show ?case
by (cases t) auto
qed auto

text â¹Simplification rules on @{const hole_pos}âº

lemma hole_pos_map_vars [simp]:
"hole_pos (map_vars_ctxt f C) = hole_pos C"
by (induct C) auto

lemma hole_pos_in_ctxt_apply [simp]: "hole_pos C â poss Câ¨uâ©"
by (induct C) auto

subsection â¹Properties of @{const ground} and @{const ground_ctxt}âº

lemma ground_vars_term_empty [simp]:
"ground t â¹ vars_term t = {}"
by (induct t) auto

lemma ground_map_term [simp]:
"ground (map_term f h t) = ground t"
by (induct t) auto

lemma ground_ctxt_apply [simp]:
"ground Câ¨tâ© â· ground_ctxt C â§ ground t"
by (induct C) auto

lemma ground_ctxt_comp [intro]:
"ground_ctxt C â¹ ground_ctxt D â¹ ground_ctxt (C ââ©c D)"
by (induct C) auto

lemma ctxt_comp_n_pres_ground [intro]:
"ground_ctxt C â¹ ground_ctxt (C^n)"
by (induct n arbitrary: C) auto

lemma subterm_eq_pres_ground:
assumes "ground s" and "s âµ t"
shows "ground t" using assms(2,1)
by (induct) auto

lemma ground_substD:
"ground (l â Ï) â¹ x â vars_term l â¹ ground (Ï x)"
by (induct l) auto

lemma ground_substI:
"(â x. x â vars_term s â¹ ground (Ï x)) â¹ ground (s â Ï)"
by (induct s) auto

subsection â¹Properties on signature induced by a term @{type term}/context @{type ctxt}âº

lemma funas_ctxt_apply [simp]:
"funas_term Câ¨tâ© = funas_ctxt C âª funas_term t"
by (induct C) auto

lemma funas_term_map [simp]:
"funas_term (map_term f h t) = (Î» (g, n). (f g, n))  funas_term t"
by (induct t) auto

lemma funas_term_subst:
"funas_term (l â Ï) = funas_term l âª (â (funas_term  Ï  vars_term l))"
by (induct l) auto

lemma funas_ctxt_comp [simp]:
"funas_ctxt (C ââ©c D) = funas_ctxt C âª funas_ctxt D"
by (induct C) auto

lemma ctxt_comp_n_funas [simp]:
"(f, v) â funas_ctxt (C^n) â¹ (f, v) â funas_ctxt C"
by (induct n arbitrary: C) auto

lemma ctxt_comp_n_pres_funas [intro]:
"funas_ctxt C â â± â¹ funas_ctxt (C^n) â â±"
by (induct n arbitrary: C) auto

subsection â¹Properties on subterm at given position @{const subt_at}âº

lemma subt_at_Cons_comp:
"i # p â poss s â¹ (s |_ [i]) |_ p = s |_ (i # p)"
by (cases s) auto

lemma ctxt_at_pos_subt_at_pos:
"p â poss t â¹ (ctxt_at_pos t p)â¨uâ© |_ p = u"
proof (induct p arbitrary: t)
case (Cons i p)
then show ?case using id_take_nth_drop
by (cases t) (auto simp: nth_append)
qed auto

lemma ctxt_at_pos_subt_at_id:
"p â poss t â¹ (ctxt_at_pos t p)â¨t |_ pâ© = t"
proof (induct p arbitrary: t)
case (Cons i p)
then show ?case using id_take_nth_drop
by (cases t) force+
qed auto

lemma subst_at_ctxt_at_eq_termD:
assumes "s = t" "p â poss t"
shows "s |_ p = t |_ p â§ ctxt_at_pos s p = ctxt_at_pos t p" using assms
by auto

lemma subst_at_ctxt_at_eq_termI:
assumes "p â poss s" "p â poss t"
and "s |_p = t |_ p"
and "ctxt_at_pos s p = ctxt_at_pos t p"
shows "s = t" using assms
by (metis ctxt_at_pos_subt_at_id)

lemma subt_at_subterm_eq [intro!]:
"p â poss t â¹ t âµ t |_ p"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons(1)[of "args t ! i"] Cons(2) show ?case
by (cases t) force+
qed auto

lemma subt_at_subterm [intro!]:
"p â poss t â¹ p â  [] â¹  t â³ t |_ p"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons(1)[of "args t ! i"] Cons(2) show ?case
by (cases t) force+
qed auto

lemma ctxt_at_pos_hole_pos [simp]: "ctxt_at_pos Câ¨sâ© (hole_pos C) = C"
by (induct C) auto

subsection â¹Properties on replace terms at a given position
@{const replace_term_at}âº

lemma replace_term_at_not_poss [simp]:
"p â poss s â¹ s[p â t] = s"
proof (induct s arbitrary: p)
case (Var x) then show ?case by (cases p) auto
next
case (Fun f ts) show ?case using Fun(1)[OF nth_mem] Fun(2)
by (cases p) (auto simp: min_def intro!: nth_equalityI)
qed

lemma replace_term_at_replace_at_conv:
"p â poss s â¹ (ctxt_at_pos s p)â¨tâ© = s[p â t]"
by (induct s arbitrary: p) (auto simp: upd_conv_take_nth_drop)

lemma parallel_replace_term_commute [ac_simps]:
"p â¥ q â¹ s[p â t][q â u] = s[q â u][p â t]"
proof (induct s arbitrary: p q)
case (Var x) then show ?case
by (cases p; cases q) auto
next
case (Fun f ts)
from Fun(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 â¹ (Fun f ts)[p â t][q â u] = (Fun f ts)[q â u][p â t]"
by (auto simp: list_update_swap)
then show ?case using Fun(1)[OF nth_mem, of j ps qs] Fun(2)
by (cases "i = j") (auto simp: par_Cons_iff)
qed

lemma replace_term_at_above [simp]:
"p â¤â©p q â¹ s[q â t][p â u] = s[p â u]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto

lemma replace_term_at_below [simp]:
"p <â©p q â¹ s[p â t][q â u] = s[p â t[q -â©p p â u]]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto

lemma replace_at_hole_pos [simp]: "Câ¨sâ©[hole_pos C â t] = Câ¨tâ©"
by (induct C) auto

subsection â¹Properties on @{const adapt_vars} and @{const adapt_vars_ctxt}âº

by (induct t) (auto simp add: adapt_vars_def)

lemma adapt_vars_simps[code, simp]: "adapt_vars (Fun f ts) = Fun f (map adapt_vars ts)"
by (induct ts, auto simp: adapt_vars_def)

lemma adapt_vars_reverse: "ground t â¹ adapt_vars t' = t â¹ adapt_vars t = t'"
proof (induct t arbitrary: t')
case (Fun f ts)
then show ?case by (cases t') (auto simp add: map_idI)
qed auto

lemma ground_adapt_vars [simp]: "ground (adapt_vars t) = ground t"

assumes g: "ground t"
shows "adapt_vars (adapt_vars t :: ('f,'w)term) = t"
proof -
let ?t' = "adapt_vars t :: ('f,'w)term"
have gt': "ground ?t'" using g by auto
from adapt_vars_reverse[OF gt', of t] show ?thesis by blast
qed

assumes "adapt_vars x = adapt_vars y" "ground x" "ground y"
shows "x = y"

"adapt_vars_ctxt (More f bef C aft) = More f (map adapt_vars bef) (adapt_vars_ctxt C) (map adapt_vars aft)"

by (induct C, auto)

lemma adapt_vars_subst[simp]: "adapt_vars (l â Ï) = l â (Î» x. adapt_vars (Ï x))"
by (induct l) auto

"ground t â¹ map_vars_term f t = adapt_vars t"
by (induct t) auto

"ground_ctxt C â¹ map_vars_ctxt f C = adapt_vars_ctxt C"
by (induct C) auto

subsubsection â¹Equality on ground terms/contexts by positions and symbolsâº

lemma fun_at_def':
"fun_at t p = (if p â poss t then
(case t |_ p of Var x â Some (Inr x) | Fun f ts â Some (Inl f)) else None)"
by (induct t p rule: fun_at.induct) auto

lemma fun_at_None_nposs_iff:
"fun_at t p = None â· p â poss t"
by (auto simp: fun_at_def') (meson term.case_eq_if)

lemma eq_term_by_poss_fun_at:
assumes "poss s = poss t" "âp. p â poss s â¹ fun_at s p = fun_at t p"
shows "s = t"
using assms
proof (induct s arbitrary: t)
case (Var x) then show ?case
by (cases t) simp_all
next
case (Fun f ss) note Fun' = this
show ?case
proof (cases t)
case (Var x) show ?thesis using Fun'(3)[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 Nil_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'(2) Fun'(3)[of "[]"] Fun'(3)[of "_ # _ :: pos"]
by (auto simp: Fun intro!: nth_equalityI Fun'(1)[OF nth_mem, of n "ts ! n" for n])
qed
qed

lemma eq_ctxt_at_pos_by_poss:
assumes "p â poss s" "p â poss t"
and "â q. Â¬ (p â¤â©p q) â¹ q â poss s â· q â poss t"
and "(â q. q â poss s â¹ Â¬ (p â¤â©p q) â¹ fun_at s q = fun_at t q)"
shows "ctxt_at_pos s p = ctxt_at_pos t p" using assms
proof (induct p arbitrary: s t)
case (Cons i p)
from Cons(2, 3) Cons(4, 5)[of "[]"] obtain f ss ts where [simp]: "s = Fun f ss" "t = Fun f ts"
by (cases s; cases t) auto
have flt: "j < i â¹ j # q â poss s â¹ fun_at s (j # q) = fun_at t (j # q)" for j q
by (intro Cons(5)) auto
have fgt: "i < j â¹ j # q â poss s â¹ fun_at s (j # q) = fun_at t (j # q)" for j q
by (intro Cons(5)) auto
have lt: "j < i â¹ j # q â poss s â· j # q â poss t" for j q by (intro Cons(4)) auto
have gt: "i < j â¹ j # q â poss s â· j # q â poss t" for j q by (intro Cons(4)) auto
from this[of _ "[]"] have "i < j â¹ j < length ss â· j < length ts" for j by auto
from this Cons(2, 3) have l: "length ss = length ts" by auto (meson nat_neq_iff)
have "ctxt_at_pos (ss ! i) p = ctxt_at_pos (ts ! i) p" using Cons(2, 3) Cons(4-)[of "i # q" for q]
by (intro Cons(1)[of "ss ! i" "ts ! i"]) auto
moreover have "take i ss = take i ts" using l lt Cons(2, 3) flt
by (intro nth_equalityI) (auto intro!: eq_term_by_poss_fun_at)
moreover have "drop (Suc i) ss = drop (Suc i) ts" using l Cons(2, 3) fgt gt[of "Suc i + j" for j]
by (intro nth_equalityI) (auto simp: nth_map intro!: eq_term_by_poss_fun_at, fastforce+)
ultimately show ?case by auto
qed auto

subsection â¹Miscâº

lemma fun_at_hole_pos_ctxt_apply [simp]:
"fun_at Câ¨tâ© (hole_pos C) = fun_at t []"
by (induct C) auto

lemma vars_term_ctxt_apply [simp]:
"vars_term Câ¨tâ© = vars_ctxt C âª vars_term t"
by (induct C arbitrary: t) auto

lemma map_vars_term_ctxt_apply:
"map_vars_term f Câ¨tâ© = (map_vars_ctxt f C)â¨map_vars_term f tâ©"
by (induct C) auto

lemma map_term_replace_at_dist:
"p â poss s â¹ (map_term f g s)[p â (map_term f g t)] = map_term f g (s[p â t])"
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

end
y>

# Theory Basic_Utils

theory Basic_Utils
imports Term_Context
begin

primrec is_Inl where
"is_Inl (Inl q) â· True"
| "is_Inl (Inr q) â· False"

primrec is_Inr where
"is_Inr (Inr q) â· True"
| "is_Inr (Inl q) â· False"

fun remove_sum where
"remove_sum (Inl q) = q"
| "remove_sum (Inr q) = q"

text â¹List operationsâº

definition filter_rev_nth where
"filter_rev_nth P xs i = length (filter P (take (Suc i) xs)) - 1"

lemma filter_rev_nth_butlast:
"Â¬ P (last xs) â¹ filter_rev_nth P xs i = filter_rev_nth P (butlast xs) i"
unfolding filter_rev_nth_def
by (induct xs arbitrary: i rule: rev_induct) (auto simp add: take_Cons')

lemma filter_rev_nth_idx:
assumes "i < length xs" "P (xs ! i)" "ys = filter P xs"
shows "xs ! i = ys ! (filter_rev_nth P xs i) â§ filter_rev_nth P xs i < length ys"
using assms unfolding filter_rev_nth_def
proof (induct xs arbitrary: ys i)
case (Cons x xs) show ?case
proof (cases "P x")
case True
then obtain ys' where *:"ys = x # ys'" using Cons(4) by auto
show ?thesis using True Cons(1)[of "i - 1" ys'] Cons(2-)
unfolding *
by (cases i) (auto simp: nth_Cons' take_Suc_conv_app_nth)
next
case False
then show ?thesis using Cons(1)[of "i - 1" ys] Cons(2-)
by (auto simp: nth_Cons')
qed
qed auto

(*replace list_of_permutation_n with n_lists *)

primrec add_elem_list_lists :: "'a â 'a list â 'a list list" where
"add_elem_list_lists x [] = [[x]]"
| "add_elem_list_lists x (y # ys) = (x # y # ys) # (map ((#) y) (add_elem_list_lists x ys))"

"ys â set (add_elem_list_lists x xs) â¹ length ys = Suc (length xs)"
by (induct xs arbitrary: ys) auto

assumes "ys â set (add_elem_list_lists x xs)"
shows "â n â¤ length xs. ys = take n xs @ x # drop n xs" using assms
proof(induct xs arbitrary: ys)
case (Cons a xs)
then show ?case
by auto fastforce
qed auto

assumes "n â¤ length xs" "ys = take n xs @ x # drop n xs"
shows "ys â set (add_elem_list_lists x xs)" using assms
proof  (induct xs arbitrary: ys n)
case (Cons a xs)
then show ?case
by (cases n) (auto simp: image_iff)
qed auto

"set (add_elem_list_lists x xs) = {ys | ys n. n â¤ length xs â§ ys = take n xs @ x # drop n xs}"
by fastforce

fun list_of_permutation_element_n :: "'a â nat â 'a list â 'a list list" where
"list_of_permutation_element_n x 0 L = [[]]"
|  "list_of_permutation_element_n x (Suc n) L = concat (map (add_elem_list_lists x) (List.n_lists n L))"

lemma list_of_permutation_element_n_conv:
assumes "n â  0"
shows "set (list_of_permutation_element_n x n L) =
{xs | xs i. i < length xs â§ (â j < length xs. j â  i â¶ xs ! j â set L) â§ length xs = n â§ xs ! i = x}" (is "?Ls = ?Rs")
proof (intro equalityI)
from assms obtain j where [simp]: "n = Suc j" using assms by (cases n) auto
{fix ys assume "ys â ?Ls"
then obtain xs i where wit: "xs â set (List.n_lists j L)" "i â¤ length xs"
"ys = take i xs @ x # drop i xs"
by (auto dest: add_elem_list_listsE)
then have "i < length ys" "length ys = Suc (length xs)" "ys ! i = x"
by (auto simp: nth_append)
moreover have "â j < length ys. j â  i â¶ ys ! j â set L" using wit(1, 2)
by (auto simp: wit(3) min_def nth_append set_n_lists)
ultimately have "ys â ?Rs" using wit(1) unfolding set_n_lists
by auto}
then show "?Ls â ?Rs" by blast
next
{fix xs assume "xs â ?Rs"
then obtain i where wit: "i < length xs" "â j < length xs. j â  i â¶ xs ! j â set L"
"length xs = n" "xs ! i = x"
by blast
then have *: "xs â set (add_elem_list_lists (xs ! i) (take i xs @ drop (Suc i) xs))"
by (auto simp: min_def intro!: nth_equalityI)
(metis Cons_nth_drop_Suc Suc_pred append_Nil append_take_drop_id assms diff_le_self diff_self_eq_0 drop_take less_Suc_eq_le nat_less_le take0)
have [simp]: "x â set (take i xs) â¹ x â set L"
"x â set (drop (Suc i) xs) â¹ x â set L" for x using wit(2)
by (auto simp: set_conv_nth)
have "xs â ?Ls" using wit
by (cases "length xs")
(auto simp: set_n_lists nth_append * min_def
intro!: exI[of _ "take i xs @ drop (Suc i) xs"])}
then show "?Rs â ?Ls" by blast
qed

lemma list_of_permutation_element_n_iff:
"set (list_of_permutation_element_n x n L) =
(if n = 0 then {[]} else {xs | xs i. i < length xs â§ (â j < length xs. j â  i â¶ xs ! j â set L) â§ length xs = n â§ xs ! i = x})"
proof (cases n)
case (Suc nat)
then have [simp]: "Suc nat â  0" by auto
then show ?thesis
by (auto simp: list_of_permutation_element_n_conv)
qed auto

lemma list_of_permutation_element_n_conv':
assumes "x â set L" "0 < n"
shows "set (list_of_permutation_element_n x n L) =
{xs. set xs â insert x (set L) â§ length xs = n â§ x â set xs}"
proof -
from assms(2) have *: "n â  0" by simp
show ?thesis using assms
unfolding list_of_permutation_element_n_conv[OF *]
by (auto simp: in_set_conv_nth)
(metis in_set_conv_nth insert_absorb subsetD)+
qed

text â¹Miscâº

lemma in_set_idx:
"x â set xs â¹ â i < length xs. xs ! i = x"
by (induct xs) force+

lemma set_list_subset_eq_nth_conv:
"set xs â A â· (â i < length xs. xs ! i â A)"
by (metis in_set_conv_nth subset_code(1))

lemma map_eq_nth_conv:
"map f xs = map g ys â· length xs = length ys â§ (â i < length ys. f (xs ! i) = g (ys ! i))"
using map_eq_imp_length_eq[of f xs g ys]
by (auto intro: nth_equalityI) (metis nth_map)

lemma nth_append_Cons: "(xs @ y # zs) ! i =
(if i < length xs then xs ! i else if i = length xs then y else zs ! (i - Suc (length xs)))"
by (cases i "length xs" rule: linorder_cases, auto simp: nth_append)

lemma map_prod_times:
"f  A Ã g  B = map_prod f g  (A Ã B)"
by auto

lemma trancl_full_on: "(X Ã X)â§+ = X Ã X"
using trancl_unfold_left[of "X Ã X"] trancl_unfold_right[of "X Ã X"] by auto

lemma trancl_map:
assumes simu: "âx y. (x, y) â r â¹ (f x, f y) â s"
and steps: "(x, y) â râ§+"
shows "(f x, f y) â sâ§+" using steps
proof (induct)
case (step y z) show ?case using step(3) simu[OF step(2)]
by auto
qed (auto simp: simu)

lemma trancl_map_prod_mono:
"map_both f  Râ§+ â (map_both f  R)â§+"
proof -
have "(f x, f y) â (map_both f  R)â§+" if "(x, y) â Râ§+" for x y using that
by (induct) (auto intro: trancl_into_trancl)
then show ?thesis by auto
qed

lemma trancl_map_both_Restr:
assumes "inj_on f X"
shows "(map_both f  Restr R X)â§+ = map_both f  (Restr R X)â§+"
proof -
have [simp]:
"map_prod (inv_into X f â f) (inv_into X f â f)  Restr R X = Restr R X"
using inv_into_f_f[OF assms]
by (intro equalityI subrelI)
(force simp: comp_def map_prod_def image_def split: prod.splits)+
have [simp]:
"map_prod (f â inv_into X f) (f â inv_into X f)  (map_both f  Restr R X)â§+ = (map_both f  Restr R X)â§+"
using f_inv_into_f[of _ f X] subsetD[OF trancl_mono_set[OF image_mono[of "Restr R X" "X Ã X" "map_both f"]]]
by (intro equalityI subrelI) (auto simp: map_prod_surj_on trancl_full_on comp_def rev_image_eqI)
show ?thesis using assms trancl_map_prod_mono[of f "Restr R X"]
image_mono[OF trancl_map_prod_mono[of "inv_into X f" "map_both f  Restr R X"], of "map_both f"]
by (intro equalityI) (simp_all add: image_comp map_prod.comp)
qed

lemma inj_on_trancl_map_both:
assumes "inj_on f (fst  R âª snd  R)"
shows "(map_both f  R)â§+ = map_both f  Râ§+"
proof -
have [simp]: "Restr R (fst  R âª snd  R) = R"
by (force simp: image_def)
then show ?thesis using assms
using trancl_map_both_Restr[of f "fst  R âª snd  R" R]
by simp
qed

lemma kleene_induct:
"A â X â¹ B O X â X â¹ X O C â X â¹ Bâ§* O A O Câ§* â X"
using relcomp_mono[OF compat_tr_compat[of B X] subset_refl, of "Câ§*"] compat_tr_compat[of "CÂ¯" "XÂ¯"]
relcomp_mono[OF relcomp_mono, OF subset_refl _ subset_refl, of A X "Bâ§*" "Câ§*"]
unfolding rtrancl_converse converse_relcomp[symmetric] converse_mono by blast

lemma kleene_trancl_induct:
"A â X â¹ B O X â X â¹ X O C â X â¹ Bâ§+ O A O Câ§+ â X"
using kleene_induct[of A X B C]
by (auto simp: rtrancl_eq_or_trancl)
(meson relcomp.relcompI subsetD trancl_into_rtrancl)

lemma rtrancl_Un2_separatorE:
"B O A = {} â¹ (A âª B)â§* = Aâ§* âª Aâ§* O Bâ§*"
by (metis R_O_Id empty_subsetI relcomp_distrib rtrancl_U_push rtrancl_reflcl_absorb sup_commute)

lemma trancl_Un2_separatorE:
assumes "B O A = {}"
shows "(A âª B)â§+ = Aâ§+ âª Aâ§+ O Bâ§+ âª Bâ§+" (is "?Ls = ?Rs")
proof -
{fix x y assume "(x, y) â ?Ls"
then have "(x, y) â ?Rs" using assms
proof (induct)
case (step y z)
then show ?case
by (auto simp add: trancl_into_trancl relcomp_unfold dest: tranclD2)
qed auto}
then show ?thesis
by (auto simp add: trancl_mono)
(meson sup_ge1 sup_ge2 trancl_mono trancl_trans)
qed

text â¹Sum types where both components have the same type (to create copies)âº

lemma is_InrE:
assumes "is_Inr q"
obtains p where "q = Inr p"
using assms by (cases q) auto

lemma is_InlE:
assumes "is_Inl q"
obtains p where "q = Inl p"
using assms by (cases q) auto

lemma not_is_Inr_is_Inl [simp]:
"Â¬ is_Inl t â· is_Inr t"
"Â¬ is_Inr t â· is_Inl t"
by (cases t, auto)+

lemma [simp]: "remove_sum â Inl = id" by auto

abbreviation CInl :: "'q â 'q + 'q" where "CInl â¡ Inl"
abbreviation CInr :: "'q â 'q + 'q" where "CInr â¡ Inr"

lemma inj_CInl: "inj CInl" "inj CInr" using inj_Inl inj_Inr by blast+

lemma map_prod_simp': "map_prod f g G = (f (fst G), g (snd G))"
by (auto simp add: map_prod_def split!: prod.splits)

end
dy>

# Theory 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]:
"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

lemma vars_term_of_gterm [simp]:
"vars_term (term_of_gterm t) = {}"
by (induct t) auto

lemma vars_term_of_gterm_subseteq [simp]:
"vars_term (term_of_gterm t) â Q â· True"
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)"
by (simp add: poss_gposs_mem_conv)

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 "gterm_of_term (term_of_gterm s |_ p) = gsubt_at s p"
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]:
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]:
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 = "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 (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 :: "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.âº
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]
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

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

lemma funas_gterm_gsubt_at_subseteq:
assumes "p â gposs s"
shows "funas_gterm (gsubt_at s p) â funas_gterm s" 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 â±"

"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

"funas_gterm s â â± â¹ s â ð¯â©G â± "
by (induct s) (auto simp: SUP_le_iff)

"s â ð¯â©G â± â· funas_gterm s â â±"

"ð¯â©G â± = gterms â±"
using ð¯â©G_funas_gterm_conv by auto

"s â ð¯â©G â± â¹ s â ð¯â©G ð¢ â¹ s â ð¯â©G (â± â© ð¢)"

"ð¢ â â± â¹ ð¯â©G ð¢ â ð¯â©G â±"

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
>

# Theory FSet_Utils

theory FSet_Utils
imports "HOL-Library.FSet"
"HOL-Library.List_Lexorder"
Ground_Terms
begin

context
includes fset.lifting
begin

lift_definition fCollect :: "('a â bool) â 'a fset" is "Î» P. if finite (Collect P) then Collect P else {}"
by auto

lift_definition fSigma :: "'a fset â ('a â 'b fset) â ('a Ã 'b) fset" is Sigma
by auto

lift_definition is_fempty :: "'a fset â bool" is Set.is_empty .
lift_definition fremove :: "'a â 'a fset â 'a fset" is Set.remove
by (simp add: remove_def)

lift_definition finj_on :: "('a â 'b) â 'a fset â bool" is inj_on .
lift_definition the_finv_into  :: "'a fset â ('a â 'b) â 'b â 'a" is the_inv_into .

lemma fCollect_memberI [intro!]:
"finite (Collect P) â¹ P x â¹ x |â| fCollect P"
by transfer auto

lemma fCollect_member [iff]:
"x |â| fCollect P â· finite (Collect P) â§ P x"
by transfer (auto split: if_splits)

lemma fCollect_cong: "(âx. P x = Q x) â¹ fCollect P = fCollect Q"
by presburger
end

syntax
"_fColl" :: "pttrn â bool â 'a set"    ("(1{|_./ _|})")
translations
"{|x. P|}" â "CONST fCollect (Î»x. P)"

syntax (ASCII)
"_fCollect" :: "pttrn â 'a set â bool â 'a set"  ("(1{(_/|:| _)./ _})")
syntax
"_fCollect" :: "pttrn â 'a set â bool â 'a set"  ("(1{(_/ |â| _)./ _})")
translations
"{p|:|A. P}" â "CONST fCollect (Î»p. p |â| A â§ P)"

syntax (ASCII)
"_fBall"       :: "pttrn â 'a set â bool â bool"      ("(3ALL (_/|:|_)./ _)" [0, 0, 10] 10)
"_fBex"        :: "pttrn â 'a set â bool â bool"      ("(3EX (_/|:|_)./ _)" [0, 0, 10] 10)

syntax (input)
"_fBall"       :: "pttrn â 'a set â bool â bool"      ("(3! (_/|:|_)./ _)" [0, 0, 10] 10)
"_fBex"        :: "pttrn â 'a set â bool â bool"      ("(3? (_/|:|_)./ _)" [0, 0, 10] 10)

syntax
"_fBall"       :: "pttrn â 'a set â bool â bool"      ("(3â(_/|â|_)./ _)" [0, 0, 10] 10)
"_fBex"        :: "pttrn â 'a set â bool â bool"      ("(3â(_/|â|_)./ _)" [0, 0, 10] 10)

translations
"âx|â|A. P" â "CONST fBall A (Î»x. P)"
"âx|â|A. P" â "CONST fBex A (Î»x. P)"

syntax (ASCII output)
"_setlessfAll" :: "[idt, 'a, bool] â bool"  ("(3ALL _|<|_./ _)"  [0, 0, 10] 10)
"_setlessfEx"  :: "[idt, 'a, bool] â bool"  ("(3EX _|<|_./ _)"  [0, 0, 10] 10)
"_setlefAll"   :: "[idt, 'a, bool] â bool"  ("(3ALL _|<=|_./ _)" [0, 0, 10] 10)
"_setlefEx"    :: "[idt, 'a, bool] â bool"  ("(3EX _|<=|_./ _)" [0, 0, 10] 10)

syntax
"_setlessfAll" :: "[idt, 'a, bool] â bool"   ("(3â_|â|_./ _)"  [0, 0, 10] 10)
"_setlessfEx"  :: "[idt, 'a, bool] â bool"   ("(3â_|â|_./ _)"  [0, 0, 10] 10)
"_setlefAll"   :: "[idt, 'a, bool] â bool"   ("(3â_|â|_./ _)" [0, 0, 10] 10)
"_setlefEx"    :: "[idt, 'a, bool] â bool"   ("(3â_|â|_./ _)" [0, 0, 10] 10)

translations
"âA|â|B. P" â "âA. A |â| B â¶ P"
"âA|â|B. P" â "âA. A |â| B â§ P"
"âA|â|B. P" â "âA. A |â| B â¶ P"
"âA|â|B. P" â "âA. A |â| B â§ P"

syntax
"_fSetcompr" :: "'a â idts â bool â 'a fset"    ("(1{|_ |/_./ _|})")

parse_translation â¹
let
val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", \<^const_syntax>â¹Exâº));

fun nvars (Const (\<^syntax_const>â¹_idtsâº, _) $_$ idts) = nvars idts + 1
| nvars _ = 1;

fun setcompr_tr ctxt [e, idts, b] =
let
val eq = Syntax.const \<^const_syntax>â¹HOL.eqâº $Bound (nvars idts)$ e;
val P = Syntax.const \<^const_syntax>â¹HOL.conjâº $eq$ b;
val exP = ex_tr ctxt [idts, P];
in Syntax.const \<^const_syntax>â¹fCollectâº $absdummy dummyT exP end; in [(\<^syntax_const>â¹_fSetcomprâº, setcompr_tr)] end âº print_translation â¹ [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>â¹fBallâº \<^syntax_const>â¹_fBallâº, Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>â¹fBexâº \<^syntax_const>â¹_fBexâº] âº â â¹to avoid eta-contraction of bodyâº print_translation â¹ let val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (\<^const_syntax>â¹Exâº, "DUMMY")); fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] = let fun check (Const (\<^const_syntax>â¹Exâº, _)$ Abs (_, _, P), n) = check (P, n + 1)
| check (Const (\<^const_syntax>â¹HOL.conjâº, _) $(Const (\<^const_syntax>â¹HOL.eqâº, _)$ Bound m $e)$ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (=) (0 upto (n - 1), add_loose_bnos (e, 0, []))
| check _ = false;

fun tr' (_ $abs) = let val _$ idts $(_$ (_ $_$ e) $Q) = ex_tr' ctxt [abs] in Syntax.const \<^syntax_const>â¹_fSetcomprâº$ e $idts$ Q end;
in
if check (P, 0) then tr' P
else
let
val (x as _ $Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs; val M = Syntax.const \<^syntax_const>â¹_fCollâº$ x $t; in case t of Const (\<^const_syntax>â¹HOL.conjâº, _)$
(Const (\<^const_syntax>â¹fmemberâº, _) $(Const (\<^syntax_const>â¹_boundâº, _)$ Free (yN, _)) $A)$ P =>
if xN = yN then Syntax.const \<^syntax_const>â¹_fCollectâº $x$ A \$ P else M
| _ => M
end
end;
in [(\<^const_syntax>â¹fCollectâº, setcompr_tr')] end
âº

syntax
"_fSigma" :: "pttrn â 'a fset â 'b fset â ('a Ã 'b) set"  ("(3fSIGMA _|:|_./ _)" [0, 0, 10] 10)
translations
"fSIGMA x|:|A. B" â "CONST fSigma A (Î»x. B)"

notation
ffUnion ("|â|")

context
includes fset.lifting
begin

lemma right_total_cr_fset [transfer_rule]:
"right_total cr_fset"
by (auto simp: cr_fset_def right_total_def)

lemma bi_unique_cr_fset [transfer_rule]:
"bi_unique cr_fset"
by (auto simp: bi_unique_def cr_fset_def fset_inject)

lemma right_total_pcr_fset_eq [transfer_rule]:
"right_total (pcr_fset (=))"
by (simp add: right_total_cr_fset fset.pcr_cr_eq)

lemma bi_unique_pcr_fset [transfer_rule]:
"bi_unique (pcr_fset (=))"
by (simp add: fset.pcr_cr_eq bi_unique_cr_fset)

lemma set_fset_of_list_transfer [transfer_rule]:
"rel_fun (list_all2 A) (pcr_fset A) set fset_of_list"
unfolding pcr_fset_def rel_set_def rel_fun_def
by (force simp: list_all2_conv_all_nth in_set_conv_nth cr_fset_def fset_of_list.rep_eq relcompp_apply)

lemma fCollectD: "a |â| {|x . P x|} â¹ P a"
by transfer (auto split: if_splits)

lemma fCollectI: "P a â¹ finite (Collect P) â¹ a |â| {| x. P x|}"
by (auto intro: fCollect_memberI)

lemma fCollect_fempty_eq [simp]: "fCollect P = {||} â· (âx. Â¬ P x) â¨ infinite (Collect P)"
by auto

lemma fempty_fCollect_eq [simp]: "{||} = fCollect P â· (âx. Â¬ P x) â¨ infinite (Collect P)"
by auto

lemma fset_image_conv:
"{f x | x. x |â| T} = fset (f || T)"
by transfer auto

lemma fimage_def:
"f || A = {| y. âx|â|A. y = f x |}"
by transfer auto

lemma ffilter_simp: "ffilter P A = {a |â| A. P a}"
by transfer auto

lemmas fset_list_fsubset_eq_nth_conv = set_list_subset_eq_nth_conv[Transfer.transferred]
lemmas mem_idx_fset_sound = mem_idx_sound[Transfer.transferred]
â â¹Dealing with fset productsâº

abbreviation fTimes :: "'a fset â 'b fset â ('a Ã 'b) fset"  (infixr "|Ã|" 80)
where "A |Ã| B â¡ fSigma A (Î»_. B)"

lemma fSigma_repeq:
"fset (A |Ã| B) = fset A Ã fset B"
by (transfer) auto

lemmas fSigmaI [intro!] = SigmaI[Transfer.transferred]
lemmas fSigmaE [elim!] = SigmaE[Transfer.transferred]
lemmas fSigmaE2 = SigmaE2[Transfer.transferred]
lemmas fSigma_cong = Sigma_cong[Transfer.transferred]
lemmas fSigma_mono = Sigma_mono[Transfer.transferred]
lemmas fSigma_empty1 [simp] = Sigma_empty1[Transfer.transferred]
lemmas fSigma_empty2 [simp] = Sigma_empty2[Transfer.transferred]
lemmas fmem_Sigma_iff [iff] = mem_Sigma_iff[Transfer.transferred]
lemmas fmem_Times_iff = mem_Times_iff[Transfer.transferred]
lemmas fSigma_empty_iff = Sigma_empty_iff[Transfer.transferred]
lemmas fTimes_subset_cancel2 = Times_subset_cancel2[Transfer.transferred]
lemmas fTimes_eq_cancel2 = Times_eq_cancel2[Transfer.transferred]
lemmas fUN_Times_distrib = UN_Times_distrib[Transfer.transferred]
lemmas fsplit_paired_Ball_Sigma [simp, no_atp] = split_paired_Ball_Sigma[Transfer.transferred]
lemmas fsplit_paired_Bex_Sigma [simp, no_atp] = split_paired_Bex_Sigma[Transfer.transferred]
lemmas fSigma_Un_distrib1 = Sigma_Un_distrib1[Transfer.transferred]
lemmas fSigma_Un_distrib2 = Sigma_Un_distrib2[Transfer.transferred]
lemmas fSigma_Int_distrib1 = Sigma_Int_distrib1[Transfer.transferred]
lemmas fSigma_Int_distrib2 = Sigma_Int_distrib2[Transfer.transferred]
lemmas fSigma_Diff_distrib1 = Sigma_Diff_distrib1[Transfer.transferred]
lemmas fSigma_Diff_distrib2 = Sigma_Diff_distrib2[Transfer.transferred]
lemmas fSigma_Union = Sigma_Union[Transfer.transferred]
lemmas fTimes_Un_distrib1 = Times_Un_distrib1[Transfer.transferred]
lemmas fTimes_Int_distrib1 = Times_Int_distrib1[Transfer.transferred]
lemmas fTimes_Diff_distrib1 = Times_Diff_distrib1[Transfer.transferred]
lemmas fTimes_empty [simp] = Times_empty[Transfer.transferred]
lemmas ftimes_subset_iff = times_subset_iff[Transfer.transferred]
lemmas ftimes_eq_iff = times_eq_iff[Transfer.transferred]
lemmas ffst_image_times [simp] = fst_image_times[Transfer.transferred]
lemmas fsnd_image_times [simp] = snd_image_times[Transfer.transferred]
lemmas fsnd_image_Sigma = snd_image_Sigma[Transfer.transferred]
lemmas finsert_Times_insert = insert_Times_insert[Transfer.transferred]
lemmas fTimes_Int_Times =`