# 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
*)

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,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]:
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