Theory Term_Abstraction

(*  Title:      Term_Abstraction.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, University of Exeter
    Author:     Anders Schlichtkrull, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section‹Term Abstraction›
theory Term_Abstraction
  imports Transactions
begin

subsection ‹Definitions›
fun to_abs ("α0") where
  "α0 [] _ = {}"
| "α0 ((Fun (Val m) [],Fun (Set s) S)#D) n =
    (if m = n then insert s (α0 D n) else α0 D n)"
| "α0 (_#D) n = α0 D n"

fun abs_apply_term (infixl "⋅α" 67) where
  "Var x ⋅α α = Var x"
| "Fun (Val n) T ⋅α α = Fun (Abs (α n)) (map (λt. t ⋅α α) T)"
| "Fun f T ⋅α α = Fun f (map (λt. t ⋅α α) T)"

definition abs_apply_list (infixl "⋅αlist" 67) where
  "M ⋅αlist α ≡ map (λt. t ⋅α α) M"

definition abs_apply_terms (infixl "⋅αset" 67) where
  "M ⋅αset α ≡ (λt. t ⋅α α) ` M"

definition abs_apply_pairs (infixl "⋅αpairs" 67) where
  "F ⋅αpairs α ≡ map (λ(s,t). (s ⋅α α, t ⋅α α)) F"

definition abs_apply_strand_step (infixl "⋅αstp" 67) where
  "s ⋅αstp α ≡ (case s of
    (l,send⟨ts⟩) ⇒ (l,send⟨ts ⋅αlist α⟩)
  | (l,receive⟨ts⟩) ⇒ (l,receive⟨ts ⋅αlist α⟩)
  | (l,⟨ac: t ≐ t'⟩) ⇒ (l,⟨ac: (t ⋅α α) ≐ (t' ⋅α α)⟩)
  | (l,insert⟨t,t'⟩) ⇒ (l,insert⟨t ⋅α α,t' ⋅α α⟩)
  | (l,delete⟨t,t'⟩) ⇒ (l,delete⟨t ⋅α α,t' ⋅α α⟩)
  | (l,⟨ac: t ∈ t'⟩) ⇒ (l,⟨ac: (t ⋅α α) ∈ (t' ⋅α α)⟩)
  | (l,∀X⟨∨≠: F ∨∉: F'⟩) ⇒ (l,∀X⟨∨≠: (F ⋅αpairs α) ∨∉: (F' ⋅αpairs α)⟩))"

definition abs_apply_strand (infixl "⋅αst" 67) where
  "S ⋅αst α ≡ map (λx. x ⋅αstp α) S"


subsection ‹Lemmata›
lemma to_abs_alt_def:
  "α0 D n = {s. ∃S. (Fun (Val n) [], Fun (Set s) S) ∈ set D}"
by (induct D n rule: to_abs.induct) auto

lemma abs_term_apply_const[simp]:
  "is_Val f ⟹ Fun f [] ⋅α a = Fun (Abs (a (the_Val f))) []"
  "¬is_Val f ⟹ Fun f [] ⋅α a = Fun f []"
by (cases f; auto)+

lemma abs_fv: "fv (t ⋅α a) = fv t"
by (induct t a rule: abs_apply_term.induct) auto

lemma abs_eq_if_no_Val:
  assumes "∀f ∈ funs_term t. ¬is_Val f"
  shows "t ⋅α a = t ⋅α b"
using assms
proof (induction t)
  case (Fun f T) thus ?case by (cases f) simp_all
qed simp

lemma abs_list_set_is_set_abs_set: "set (M ⋅αlist α) = (set M) ⋅αset α"
unfolding abs_apply_list_def abs_apply_terms_def by simp

lemma abs_set_empty[simp]: "{} ⋅αset α = {}"
unfolding abs_apply_terms_def by simp

lemma abs_in:
  assumes "t ∈ M"
  shows "t ⋅α α ∈ M ⋅αset α"
using assms unfolding abs_apply_terms_def
by (induct t α rule: abs_apply_term.induct) blast+

lemma abs_set_union: "(A ∪ B) ⋅αset a = (A ⋅αset a) ∪ (B ⋅αset a)"
unfolding abs_apply_terms_def
by auto

lemma abs_subterms: "subterms (t ⋅α α) = subterms t ⋅αset α"
proof (induction t)
  case (Fun f T) thus ?case by (cases f) (auto simp add: abs_apply_terms_def)
qed (simp add: abs_apply_terms_def)

lemma abs_subterms_in: "s ∈ subterms t ⟹ s ⋅α a ∈ subterms (t ⋅α a)"
proof (induction t)
  case (Fun f T) thus ?case by (cases f) auto
qed simp

lemma abs_ik_append: "(iksst (A@B) ⋅set I) ⋅αset a = (iksst A ⋅set I) ⋅αset a ∪ (iksst B ⋅set I) ⋅αset a"
unfolding abs_apply_terms_def iksst_def
by fastforce

lemma to_abs_in:
  assumes "(Fun (Val n) [], Fun (Set s) []) ∈ set D"
  shows "s ∈ α0 D n"
using assms by (induct rule: to_abs.induct) auto

lemma to_abs_empty_iff_notin_db:
  "Fun (Val n) [] ⋅α α0 D = Fun (Abs {}) [] ⟷ (∄s S. (Fun (Val n) [], Fun (Set s) S) ∈ set D)"
by (simp add: to_abs_alt_def)

lemma to_abs_list_insert:
  assumes "Fun (Val n) [] ≠ t"
  shows "α0 D n = α0 (List.insert (t,s) D) n"
using assms to_abs_alt_def[of D n] to_abs_alt_def[of "List.insert (t,s) D" n]
by auto

lemma to_abs_list_insert':
  "insert s (α0 D n) = α0 (List.insert (Fun (Val n) [], Fun (Set s) S) D) n"
using to_abs_alt_def[of D n]
      to_abs_alt_def[of "List.insert (Fun (Val n) [], Fun (Set s) S) D" n]
by auto

lemma to_abs_list_remove_all:
  assumes "Fun (Val n) [] ≠ t"
  shows "α0 D n = α0 (List.removeAll (t,s) D) n"
using assms to_abs_alt_def[of D n] to_abs_alt_def[of "List.removeAll (t,s) D" n]
by auto

lemma to_abs_list_remove_all':
  "α0 D n - {s} = α0 (filter (λd. ∄S. d = (Fun (Val n) [], Fun (Set s) S)) D) n"
using to_abs_alt_def[of D n]
      to_abs_alt_def[of "filter (λd. ∄S. d = (Fun (Val n) [], Fun (Set s) S)) D" n]
by auto

lemma to_abs_dbsst_append:
  assumes "∀u s. insert⟨u, s⟩ ∈ set B ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
    and "∀u s. delete⟨u, s⟩ ∈ set B ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
  shows "α0 (db'sst A ℐ D) n = α0 (db'sst (A@B) ℐ D) n"
using assms
proof (induction B rule: List.rev_induct)
  case (snoc b B)
  hence IH: "α0 (db'sst A ℐ D) n = α0 (db'sst (A@B) ℐ D) n" by auto
  have *: "∀u s. b = insert⟨u,s⟩ ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
          "∀u s. b = delete⟨u,s⟩ ⟶ Fun (Val n) [] ≠ u ⋅ ℐ"
    using snoc.prems by simp_all
  show ?case
  proof (cases b)
    case (Insert u s)
    hence **: "db'sst (A@B@[b]) ℐ D = List.insert (u ⋅ ℐ,s ⋅ ℐ) (db'sst (A@B) ℐ D)"
      using dbsst_append[of "A@B" "[b]"] by simp
    have "Fun (Val n) [] ≠ u ⋅ ℐ" using *(1) Insert by auto
    thus ?thesis using IH ** to_abs_list_insert by metis
  next
    case (Delete u s)
    hence **: "db'sst (A@B@[b]) ℐ D = List.removeAll (u ⋅ ℐ,s ⋅ ℐ) (db'sst (A@B) ℐ D)"
      using dbsst_append[of "A@B" "[b]"] by simp
    have "Fun (Val n) [] ≠ u ⋅ ℐ" using *(2) Delete by auto
    thus ?thesis using IH ** to_abs_list_remove_all by metis
  qed (simp_all add: dbsst_no_upd_append[of "[b]" "A@B"] IH)
qed simp

lemma to_abs_neq_imp_db_update:
  assumes "α0 (dbsst A I) n ≠ α0 (dbsst (A@B) I) n"
  shows "∃u s. u ⋅ I = Fun (Val n) [] ∧ (insert⟨u,s⟩ ∈ set B ∨ delete⟨u,s⟩ ∈ set B)"
proof -
  { fix D have ?thesis when "α0 D n ≠ α0 (db'sst B I D) n" using that
    proof (induction B I D rule: db'sst.induct)
      case 2 thus ?case
        by (metis db'sst.simps(2) list.set_intros(1,2) subst_apply_pair_pair to_abs_list_insert)
    next
      case 3 thus ?case
        by (metis db'sst.simps(3) list.set_intros(1,2) subst_apply_pair_pair to_abs_list_remove_all)
    qed simp_all
  } thus ?thesis using assms by (metis dbsst_append dbsst_def)
qed

lemma abs_term_subst_eq:
  fixes δ θ::"(('a,'b,'c,'d) prot_fun, ('e,'f prot_atom) term × nat) subst"
  assumes "∀x ∈ fv t. δ x ⋅α a = θ x ⋅α b"
    and "∄n T. Fun (Val n) T ∈ subterms t"
  shows "t ⋅ δ ⋅α a = t ⋅ θ ⋅α b"
using assms
proof (induction t)
  case (Fun f T) thus ?case
  proof (cases f)
    case (Val n)
    hence False using Fun.prems(2) by blast
    thus ?thesis by metis
  qed auto
qed simp

lemma abs_term_subst_eq':
  fixes δ θ::"(('a,'b,'c,'d) prot_fun, ('e,'f prot_atom) term × nat) subst"
  assumes "∀x ∈ fv t. δ x ⋅α a = θ x"
    and "∄n T. Fun (Val n) T ∈ subterms t"
  shows "t ⋅ δ ⋅α a = t ⋅ θ"
using assms
proof (induction t)
  case (Fun f T) thus ?case
  proof (cases f)
    case (Val n)
    hence False using Fun.prems(2) by blast
    thus ?thesis by metis
  qed auto
qed simp

lemma abs_val_in_funs_term:
  assumes "f ∈ funs_term t" "is_Val f"
  shows "Abs (α (the_Val f)) ∈ funs_term (t ⋅α α)"
using assms by (induct t α rule: abs_apply_term.induct) auto

end