Theory Term_Implication

(*  Title:      Term_Implication.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 Implication›
theory Term_Implication
  imports Stateful_Protocol_Model Term_Variants
begin

subsection ‹Single Term Implications›
definition timpl_apply_term ("_ --» _⟩⟨_") where
  "a --» b⟩⟨t  term_variants ((λ_. [])(Abs a := [Abs b])) t"

definition timpl_apply_terms ("_ --» _⟩⟨_set") where
  "a --» b⟩⟨Mset  ((set o timpl_apply_term a b) ` M)"

lemma timpl_apply_Fun:
  assumes "i. i < length T  S ! i  set a --» b⟩⟨T ! i"
    and "length T = length S"
  shows "Fun f S  set a --» b⟩⟨Fun f T"
using assms term_variants_Fun term_variants_pred_iff_in_term_variants
by (metis timpl_apply_term_def)

lemma timpl_apply_Abs:
  assumes "i. i < length T  S ! i  set a --» b⟩⟨T ! i"
    and "length T = length S"
  shows "Fun (Abs b) S  set a --» b⟩⟨Fun (Abs a) T"
using assms(1) term_variants_P[OF assms(2), of "(λ_. [])(Abs a := [Abs b])" "Abs b" "Abs a"]
unfolding timpl_apply_term_def term_variants_pred_iff_in_term_variants[symmetric]
by fastforce

lemma timpl_apply_refl: "t  set a --» b⟩⟨t"
unfolding timpl_apply_term_def
by (metis term_variants_pred_refl term_variants_pred_iff_in_term_variants)

lemma timpl_apply_const: "Fun (Abs b) []  set a --» b⟩⟨Fun (Abs a) []"
using term_variants_pred_iff_in_term_variants term_variants_pred_const
unfolding timpl_apply_term_def by auto

lemma timpl_apply_const':
  "c = a  set a --» b⟩⟨Fun (Abs c) [] = {Fun (Abs b) [], Fun (Abs c) []}"
  "c  a  set a --» b⟩⟨Fun (Abs c) [] = {Fun (Abs c) []}"
using term_variants_pred_const_cases[of "(λ_. [])(Abs a := [Abs b])" "Abs c"]
      term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
unfolding timpl_apply_term_def by auto

lemma timpl_apply_term_subst:
  "s  set a --» b⟩⟨t  s  δ  set a --» b⟩⟨t  δ"
by (metis term_variants_pred_iff_in_term_variants term_variants_pred_subst timpl_apply_term_def)

lemma timpl_apply_inv:
  assumes "Fun h S  set a --» b⟩⟨Fun f T"
  shows "length T = length S"
    and "i. i < length T  S ! i  set a --» b⟩⟨T ! i"
    and "f  h  f = Abs a  h = Abs b"
using assms term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
unfolding timpl_apply_term_def
by (metis (full_types) term_variants_pred_inv(1),
    metis (full_types) term_variants_pred_inv(2),
    fastforce dest: term_variants_pred_inv(3))

lemma timpl_apply_inv':
  assumes "s  set a --» b⟩⟨Fun f T"
  shows "g S. s = Fun g S"
proof -
  have *: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) (Fun f T) s"
    using assms term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
    unfolding timpl_apply_term_def by force
  show ?thesis using term_variants_pred.cases[OF *, of ?thesis] by fastforce
qed

lemma timpl_apply_term_Var_iff:
  "Var x  set a --» b⟩⟨t  t = Var x"
using term_variants_pred_inv_Var term_variants_pred_iff_in_term_variants
unfolding timpl_apply_term_def by metis



subsection ‹Term Implication Closure›
inductive_set timpl_closure for t TI where
  FP: "t  timpl_closure t TI"
| TI: "u  timpl_closure t TI; (a,b)  TI; term_variants_pred ((λ_. [])(Abs a := [Abs b])) u s
        s  timpl_closure t TI"

definition "timpl_closure_set M TI  (t  M. timpl_closure t TI)"

inductive_set timpl_closure'_step for TI where
  "(a,b)  TI; term_variants_pred ((λ_. [])(Abs a := [Abs b])) t s
     (t,s)  timpl_closure'_step TI"

definition "timpl_closure' TI  (timpl_closure'_step TI)*"

definition comp_timpl_closure where
  "comp_timpl_closure FP TI 
    let f = λX. FP  (x  X. (a,b)  TI. set a --» b⟩⟨x)
    in while (λX. f X  X) f {}"

definition comp_timpl_closure_list where
  "comp_timpl_closure_list FP TI 
    let f = λX. remdups (concat (map (λx. concat (map (λ(a,b). a --» b⟩⟨x) TI)) X)@X)
    in while (λX. set (f X)  set X) f FP"

lemma timpl_closure_setI:
  "t  M  t  timpl_closure_set M TI"
unfolding timpl_closure_set_def by (auto intro: timpl_closure.FP)

lemma timpl_closure_set_empty_timpls:
  "timpl_closure t {} = {t}" (is "?A = ?B")
proof (intro subset_antisym subsetI)
  fix s show "s  ?A  s  ?B"
    by (induct s rule: timpl_closure.induct) auto
qed (simp add: timpl_closure.FP)

lemmas timpl_closure_set_is_timpl_closure_union = meta_eq_to_obj_eq[OF timpl_closure_set_def]

lemma term_variants_pred_eq_case_Abs:
  fixes a b
  defines "P  (λ_. [])(Abs a := [Abs b])"
  assumes "term_variants_pred P t s" "f  funs_term s. ¬is_Abs f"
  shows "t = s"
using assms(2,3)
proof (induction t s rule: term_variants_pred.induct)
  case (term_variants_Fun T S f)
  have "¬is_Abs h" when i: "i < length S" and h: "h  funs_term (S ! i)" for i h
    using i h term_variants_Fun.prems by auto
  hence "T ! i = S ! i" when i: "i < length T" for i
    using i term_variants_Fun.hyps(1) term_variants_Fun.IH by auto
  hence "T = S" using term_variants_Fun.hyps(1) nth_equalityI[of T S] by fast
  thus ?case using term_variants_Fun.hyps(1) by blast
qed (simp_all add: term_variants_pred_refl P_def)

lemma timpl_closure'_step_inv:
  assumes "(t,s)  timpl_closure'_step TI"
  obtains a b where "(a,b)  TI" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) t s"
using assms by (auto elim: timpl_closure'_step.cases)

lemma timpl_closure_mono:
  assumes "TI  TI'"
  shows "timpl_closure t TI  timpl_closure t TI'"
proof
  fix s show "s  timpl_closure t TI  s  timpl_closure t TI'"
    apply (induct rule: timpl_closure.induct)
    using assms by (auto intro: timpl_closure.intros)
qed

lemma timpl_closure_set_mono:
  assumes "M  M'" "TI  TI'"
  shows "timpl_closure_set M TI  timpl_closure_set M' TI'"
using assms(1) timpl_closure_mono[OF assms(2)] unfolding timpl_closure_set_def by fast

lemma timpl_closure_idem:
  "timpl_closure_set (timpl_closure t TI) TI = timpl_closure t TI" (is "?A = ?B")
proof
  have "s  timpl_closure t TI"
    when "s  timpl_closure u TI" "u  timpl_closure t TI"
    for s u
    using that
    by (induction rule: timpl_closure.induct)
       (auto intro: timpl_closure.intros)
  thus "?A  ?B" unfolding timpl_closure_set_def by blast

  show "?B  ?A"
    unfolding timpl_closure_set_def
    by (blast intro: timpl_closure.FP)
qed

lemma timpl_closure_set_idem:
  "timpl_closure_set (timpl_closure_set M TI) TI = timpl_closure_set M TI"
using timpl_closure_idem[of _ TI]unfolding timpl_closure_set_def by auto

lemma timpl_closure_set_mono_timpl_closure_set:
  assumes N: "N  timpl_closure_set M TI"
  shows "timpl_closure_set N TI  timpl_closure_set M TI"
using timpl_closure_set_mono[OF N, of TI TI] timpl_closure_set_idem[of M TI]
by simp

lemma timpl_closure_is_timpl_closure':
  "s  timpl_closure t TI  (t,s)  timpl_closure' TI"
proof
  show "s  timpl_closure t TI  (t,s)  timpl_closure' TI"
    unfolding timpl_closure'_def
    by (induct rule: timpl_closure.induct)
       (auto intro: rtrancl_into_rtrancl timpl_closure'_step.intros)

  show "(t,s)  timpl_closure' TI  s  timpl_closure t TI"
    unfolding timpl_closure'_def
    by (induct rule: rtrancl_induct)
       (auto dest: timpl_closure'_step_inv
             intro: timpl_closure.FP timpl_closure.TI)
qed

lemma timpl_closure'_mono:
  assumes "TI  TI'"
  shows "timpl_closure' TI  timpl_closure' TI'"
using timpl_closure_mono[OF assms]
      timpl_closure_is_timpl_closure'[of _ _ TI]
      timpl_closure_is_timpl_closure'[of _ _ TI']
by fast

lemma timpl_closureton_is_timpl_closure:
  "timpl_closure_set {t} TI = timpl_closure t TI"
by (simp add: timpl_closure_set_is_timpl_closure_union)

lemma timpl_closure'_timpls_trancl_subset:
  "timpl_closure' (c+)  timpl_closure' c"
unfolding timpl_closure'_def
proof
  fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
  show "(s,t)  (timpl_closure'_step (c+))*  (s,t)  (timpl_closure'_step c)*"
  proof (induction rule: rtrancl_induct)
    case (step u t)
    obtain a b where ab:
        "(a,b)  c+" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
      using step.hyps(2) timpl_closure'_step_inv by blast
    hence "(u,t)  (timpl_closure'_step c)*"
    proof (induction arbitrary: t rule: trancl_induct)
      case (step d e)
      obtain s where s:
          "term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
          "term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
        using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast

      have "(u,s)  (timpl_closure'_step c)*"
           "(s,t)  timpl_closure'_step c"
        using step.hyps(2) s(2) step.IH[OF s(1)]
        by (auto intro: timpl_closure'_step.intros)
      thus ?case by simp
    qed (auto intro: timpl_closure'_step.intros)
    thus ?case using step.IH by simp
  qed simp
qed

lemma timpl_closure'_timpls_trancl_subset':
  "timpl_closure' {(a,b)  c+. a  b}  timpl_closure' c"
using timpl_closure'_timpls_trancl_subset
      timpl_closure'_mono[of "{(a,b)  c+. a  b}" "c+"]
by fast

lemma timpl_closure_set_timpls_trancl_subset:
  "timpl_closure_set M (c+)  timpl_closure_set M c"
using timpl_closure'_timpls_trancl_subset[of c]
      timpl_closure_is_timpl_closure'[of _ _ c]
      timpl_closure_is_timpl_closure'[of _ _ "c+"]
      timpl_closure_set_is_timpl_closure_union[of M c]
      timpl_closure_set_is_timpl_closure_union[of M "c+"]
by fastforce

lemma timpl_closure_set_timpls_trancl_subset':
  "timpl_closure_set M {(a,b)  c+. a  b}  timpl_closure_set M c"
using timpl_closure'_timpls_trancl_subset'[of c]
      timpl_closure_is_timpl_closure'[of _ _ c]
      timpl_closure_is_timpl_closure'[of _ _ "{(a,b)  c+. a  b}"]
      timpl_closure_set_is_timpl_closure_union[of M c]
      timpl_closure_set_is_timpl_closure_union[of M "{(a,b)  c+. a  b}"]
by fastforce

lemma timpl_closure'_timpls_trancl_supset':
  "timpl_closure' c  timpl_closure' {(a,b)  c+. a  b}"
unfolding timpl_closure'_def
proof
  let ?cl = "{(a,b)  c+. a  b}"

  fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
  show "(s,t)  (timpl_closure'_step c)*  (s,t)  (timpl_closure'_step ?cl)*"
  proof (induction rule: rtrancl_induct)
    case (step u t)
    obtain a b where ab:
        "(a,b)  c" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
      using step.hyps(2) timpl_closure'_step_inv by blast
    hence "(a,b)  c+" by simp
    hence "(u,t)  (timpl_closure'_step ?cl)*" using ab(2)
    proof (induction arbitrary: t rule: trancl_induct)
      case (base d) show ?case
      proof (cases "a = d")
        case True thus ?thesis
          using base term_variants_pred_refl_inv[of _ u t]
          by force
      next
        case False thus ?thesis
          using base timpl_closure'_step.intros[of a d ?cl]
          by fast
      qed
    next
      case (step d e)
      obtain s where s:
          "term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
          "term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
        using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast

      show ?case
      proof (cases "d = e")
        case True
        thus ?thesis
          using step.prems step.IH[of t]
          by blast
      next
        case False
        hence "(u,s)  (timpl_closure'_step ?cl)*"
              "(s,t)  timpl_closure'_step ?cl"
          using step.hyps(2) s(2) step.IH[OF s(1)]
          by (auto intro: timpl_closure'_step.intros)
        thus ?thesis by simp
      qed
    qed
    thus ?case using step.IH by simp
  qed simp
qed

lemma timpl_closure'_timpls_trancl_supset:
  "timpl_closure' c  timpl_closure' (c+)"
using timpl_closure'_timpls_trancl_supset'[of c]
      timpl_closure'_mono[of "{(a,b)  c+. a  b}" "c+"]
by fast

lemma timpl_closure'_timpls_trancl_eq:
  "timpl_closure' (c+) = timpl_closure' c"
using timpl_closure'_timpls_trancl_subset timpl_closure'_timpls_trancl_supset
by blast

lemma timpl_closure'_timpls_trancl_eq':
  "timpl_closure' {(a,b)  c+. a  b} = timpl_closure' c"
using timpl_closure'_timpls_trancl_subset' timpl_closure'_timpls_trancl_supset'
by blast

lemma timpl_closure'_timpls_rtrancl_subset:
  "timpl_closure' (c*)  timpl_closure' c"
unfolding timpl_closure'_def
proof
  fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
  show "(s,t)  (timpl_closure'_step (c*))*  (s,t)  (timpl_closure'_step c)*"
  proof (induction rule: rtrancl_induct)
    case (step u t)
    obtain a b where ab:
        "(a,b)  c*" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
      using step.hyps(2) timpl_closure'_step_inv by blast
    hence "(u,t)  (timpl_closure'_step c)*"
    proof (induction arbitrary: t rule: rtrancl_induct)
      case base
      hence "u = t" using term_variants_pred_refl_inv by fastforce
      thus ?case by simp
    next
      case (step d e)
      obtain s where s:
          "term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
          "term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
        using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast

      have "(u,s)  (timpl_closure'_step c)*"
           "(s,t)  timpl_closure'_step c"
        using step.hyps(2) s(2) step.IH[OF s(1)]
        by (auto intro: timpl_closure'_step.intros)
      thus ?case by simp
    qed
    thus ?case using step.IH by simp
  qed simp
qed

lemma timpl_closure'_timpls_rtrancl_supset:
  "timpl_closure' c  timpl_closure' (c*)"
unfolding timpl_closure'_def
proof
  fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
  show "(s,t)  (timpl_closure'_step c)*  (s,t)  (timpl_closure'_step (c*))*"
  proof (induction rule: rtrancl_induct)
    case (step u t)
    obtain a b where ab:
        "(a,b)  c" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
      using step.hyps(2) timpl_closure'_step_inv by blast
    hence "(a,b)  c*" by simp
    hence "(u,t)  (timpl_closure'_step (c*))*" using ab(2)
    proof (induction arbitrary: t rule: rtrancl_induct)
      case (base t) thus ?case using term_variants_pred_refl_inv[of _ u t] by fastforce
    next
      case (step d e)
      obtain s where s:
          "term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
          "term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
        using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast

      show ?case
      proof (cases "d = e")
        case True
        thus ?thesis
          using step.prems step.IH[of t]
          by blast
      next
        case False
        hence "(u,s)  (timpl_closure'_step (c*))*"
              "(s,t)  timpl_closure'_step (c*)"
          using step.hyps(2) s(2) step.IH[OF s(1)]
          by (auto intro: timpl_closure'_step.intros)
        thus ?thesis by simp
      qed
    qed
    thus ?case using step.IH by simp
  qed simp
qed

lemma timpl_closure'_timpls_rtrancl_eq:
  "timpl_closure' (c*) = timpl_closure' c"
using timpl_closure'_timpls_rtrancl_subset timpl_closure'_timpls_rtrancl_supset
by blast

lemma timpl_closure_timpls_trancl_eq:
  "timpl_closure t (c+) = timpl_closure t c"
using timpl_closure'_timpls_trancl_eq[of c]
      timpl_closure_is_timpl_closure'[of _ _ c]
      timpl_closure_is_timpl_closure'[of _ _ "c+"]
by fastforce

lemma timpl_closure_set_timpls_trancl_eq:
  "timpl_closure_set M (c+) = timpl_closure_set M c"
using timpl_closure_timpls_trancl_eq
      timpl_closure_set_is_timpl_closure_union[of M c]
      timpl_closure_set_is_timpl_closure_union[of M "c+"]
by fastforce

lemma timpl_closure_set_timpls_trancl_eq':
  "timpl_closure_set M {(a,b)  c+. a  b} = timpl_closure_set M c"
using timpl_closure'_timpls_trancl_eq'[of c]
      timpl_closure_is_timpl_closure'[of _ _ c]
      timpl_closure_is_timpl_closure'[of _ _ "{(a,b)  c+. a  b}"]
      timpl_closure_set_is_timpl_closure_union[of M c]
      timpl_closure_set_is_timpl_closure_union[of M "{(a,b)  c+. a  b}"]
by fastforce

lemma timpl_closure_Var_in_iff:
  "Var x  timpl_closure t TI  t = Var x" (is "?A  ?B")
proof
  have "s  timpl_closure t TI  s = Var x  s = t" for s
    apply (induction rule: timpl_closure.induct)
    by (simp, metis term_variants_pred_inv_Var(2))
  thus "?A  ?B" by blast
qed (blast intro: timpl_closure.FP)

lemma timpl_closure_set_Var_in_iff:
  "Var x  timpl_closure_set M TI  Var x  M"
unfolding timpl_closure_set_def by (simp add: timpl_closure_Var_in_iff[of x _ TI]) 

lemma timpl_closure_Var_inv:
  assumes "t  timpl_closure (Var x) TI"
  shows "t = Var x"
using assms
proof (induction rule: timpl_closure.induct)
  case (TI u a b s) thus ?case using term_variants_pred_inv_Var by fast
qed simp

lemma timpls_Un_mono: "mono (λX. FP  (x  X. (a,b)  TI. set a --» b⟩⟨x))"
by (auto intro!: monoI)

lemma timpl_closure_set_lfp:
  fixes M TI
  defines "f  λX. M  (x  X. (a,b)  TI. set a --» b⟩⟨x)"
  shows "lfp f = timpl_closure_set M TI"
proof
  note 0 = timpls_Un_mono[of M TI, unfolded f_def[symmetric]]

  let ?N = "timpl_closure_set M TI"

  show "lfp f  ?N"
  proof (induction rule: lfp_induct)
    case 2 thus ?case
    proof
      fix t assume "t  f (lfp f  ?N)"
      hence "t  M  t  (x  ?N. (a,b)  TI. set a --» b⟩⟨x)" (is "?A  ?B")
        unfolding f_def by blast
      thus "t  ?N"
      proof
        assume ?B
        then obtain s a b where s: "s  ?N" "(a,b)  TI" "t  set a --» b⟩⟨s" by moura
        thus ?thesis 
          using term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])" s]
          unfolding timpl_closure_set_def timpl_apply_term_def
          by (auto intro: timpl_closure.intros)
      qed (auto simp add: timpl_closure_set_def intro: timpl_closure.intros)
    qed
  qed (rule 0)

  have "t  lfp f" when t: "t  timpl_closure s TI" and s: "s  M" for t s
    using t
  proof (induction t rule: timpl_closure.induct)
    case (TI u a b v) thus ?case 
      using term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
            lfp_fixpoint[OF 0]
      unfolding timpl_apply_term_def f_def by fastforce
  qed (use s lfp_fixpoint[OF 0] f_def in blast)
  thus "?N  lfp f" unfolding timpl_closure_set_def by blast
qed

lemma timpl_closure_set_supset:
  assumes "t  FP. t  closure"
  and "t  closure. (a,b)  TI. s  set a --» b⟩⟨t. s  closure"
  shows "timpl_closure_set FP TI  closure"
proof -
  have "t  closure" when t: "t  timpl_closure s TI" and s: "s  FP" for t s
    using t
  proof (induction rule: timpl_closure.induct)
    case FP thus ?case using s assms(1) by blast
  next
    case (TI u a b s') thus ?case
      using assms(2) term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
      unfolding timpl_apply_term_def by fastforce
  qed
  thus ?thesis unfolding timpl_closure_set_def by blast
qed

lemma timpl_closure_set_supset':
  assumes "t  FP. (a,b)  TI. s  set a --» b⟩⟨t. s  FP"
  shows "timpl_closure_set FP TI  FP"
using timpl_closure_set_supset[OF _ assms] by blast

lemma timpl_closure'_param:
  assumes "(t,s)  timpl_closure' c"
    and fg: "f = g  (a b. (a,b)  c  f = Abs a  g = Abs b)"
  shows "(Fun f (S@t#T), Fun g (S@s#T))  timpl_closure' c"
using assms(1) unfolding timpl_closure'_def
proof (induction rule: rtrancl_induct)
  case base thus ?case
  proof (cases "f = g")
    case False
    then obtain a b where ab: "(a,b)  c" "f = Abs a" "g = Abs b"
      using fg by moura
    show ?thesis
      using term_variants_pred_param[OF term_variants_pred_refl[of "(λ_. [])(Abs a := [Abs b])" t]]
            timpl_closure'_step.intros[OF ab(1)] ab(2,3)
      by fastforce
  qed simp
next
  case (step u s)
  obtain a b where ab: "(a,b)  c" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u s"
    using timpl_closure'_step_inv[OF step.hyps(2)] by blast
  have "(Fun g (S@u#T), Fun g (S@s#T))  timpl_closure'_step c"
      using ab(1) term_variants_pred_param[OF ab(2), of g g S T]
      by (auto simp add: timpl_closure'_def intro: timpl_closure'_step.intros)
  thus ?case using rtrancl_into_rtrancl[OF step.IH] fg by blast
qed

lemma timpl_closure'_param':
  assumes "(t,s)  timpl_closure' c"
  shows "(Fun f (S@t#T), Fun f (S@s#T))  timpl_closure' c"
using timpl_closure'_param[OF assms] by simp

lemma timpl_closure_FunI:
  assumes IH: "i. i < length T  (T ! i, S ! i)  timpl_closure' c"
    and len: "length T = length S"
    and fg: "f = g  (a b. (a,b)  c+  f = Abs a  g = Abs b)"
  shows "(Fun f T, Fun g S)  timpl_closure' c"
proof -
  have aux: "(Fun f T, Fun g (take n S@drop n T))  timpl_closure' c"
    when "n  length T" for n
    using that
  proof (induction n)
    case 0
    have "(T ! n, T ! n)  timpl_closure' c" when n: "n < length T" for n
      using n unfolding timpl_closure'_def by simp
    hence "(Fun f T, Fun g T)  timpl_closure' c"
    proof (cases "f = g")
      case False
      then obtain a b where ab: "(a, b)  c+" "f = Abs a" "g = Abs b"
        using fg by moura
      show ?thesis
        using timpl_closure'_step.intros[OF ab(1), of "Fun f T" "Fun g T"] ab(2,3)
              term_variants_P[OF _ term_variants_pred_refl[of "(λ_. [])(Abs a := [Abs b])"],
                              of T g f]
              timpl_closure'_timpls_trancl_eq
        unfolding timpl_closure'_def
        by (metis fun_upd_same list.set_intros(1) r_into_rtrancl)
    qed (simp add: timpl_closure'_def)
    thus ?case by simp
  next
    case (Suc n)
    hence IH': "(Fun f T, Fun g (take n S@drop n T))  timpl_closure' c"
      and n: "n < length T" "n < length S"
      by (simp_all add: len)

    obtain T1 T2 where T: "T = T1@T ! n#T2" "length T1 = n"
      using length_prefix_ex'[OF n(1)] by auto

    obtain S1 S2 where S: "S = S1@S ! n#S2" "length S1 = n"
      using length_prefix_ex'[OF n(2)] by auto

    have "take n S@drop n T = S1@T ! n#T2" "take (Suc n) S@drop (Suc n) T = S1@S ! n#T2"
      using n T S append_eq_conv_conj
      by (metis, metis (no_types, opaque_lifting) Cons_nth_drop_Suc append.assoc append_Cons
                                             append_Nil take_Suc_conv_app_nth) 
    moreover have "(T ! n, S ! n)  timpl_closure' c" using IH Suc.prems by simp
    ultimately show ?case
      using timpl_closure'_param IH'(1)
      by (metis (no_types, lifting) timpl_closure'_def rtrancl_trans)
  qed

  show ?thesis using aux[of "length T"] len by simp
qed

lemma timpl_closure_FunI':
  assumes IH: "i. i < length T  (T ! i, S ! i)  timpl_closure' c"
    and len: "length T = length S"
  shows "(Fun f T, Fun f S)  timpl_closure' c"
using timpl_closure_FunI[OF IH len] by simp

lemma timpl_closure_FunI2:
  fixes f g::"('a, 'b, 'c, 'd) prot_fun"
  assumes IH: "i. i < length T  u. (T!i, u)  timpl_closure' c  (S!i, u)  timpl_closure' c"
    and len: "length T = length S"
    and fg: "f = g  (a b d. (a, d)  c+  (b, d)  c+  f = Abs a  g = Abs b)"
  shows "h U. (Fun f T, Fun h U)  timpl_closure' c  (Fun g S, Fun h U)  timpl_closure' c"
proof -
  let ?P = "λi u. (T ! i, u)  timpl_closure' c  (S ! i, u)  timpl_closure' c"

  define U where "U  map (λi. SOME u. ?P i u) [0..<length T]"

  have U1: "length U = length T"
    unfolding U_def by auto

  have U2: "(T ! i, U ! i)  timpl_closure' c  (S ! i, U ! i)  timpl_closure' c"
    when i: "i < length U" for i
    using i someI_ex[of "?P i"] IH[of i] U1 len
    unfolding U_def by simp

  show ?thesis
  proof (cases "f = g")
    case False
    then obtain a b d where abd: "(a, d)  c+" "(b, d)  c+" "f = Abs a" "g = Abs b"
      using fg by moura

    define h::"('a, 'b, 'c, 'd) prot_fun" where "h = Abs d"

    have "f = h  (a b. (a, b)  c+  f = Abs a  h = Abs b)"
         "g = h  (a b. (a, b)  c+  g = Abs a  h = Abs b)"
      using abd unfolding h_def by blast+
    thus ?thesis by (metis timpl_closure_FunI len U1 U2)
  qed (metis timpl_closure_FunI' len U1 U2)
qed

lemma timpl_closure_FunI3:
  fixes f g::"('a, 'b, 'c, 'd) prot_fun"
  assumes IH: "i. i < length T  u. (T!i, u)  timpl_closure' c  (S!i, u)  timpl_closure' c"
    and len: "length T = length S"
    and fg: "f = g  (a b d. (a, d)  c  (b, d)  c  f = Abs a  g = Abs b)"
  shows "h U. (Fun f T, Fun h U)  timpl_closure' c  (Fun g S, Fun h U)  timpl_closure' c"
using timpl_closure_FunI2[OF IH len] fg unfolding timpl_closure'_timpls_trancl_eq by blast

lemma timpl_closure_fv_eq:
  assumes "s  timpl_closure t T"
  shows "fv s = fv t"
using assms
by (induct rule: timpl_closure.induct)
   (metis, metis term_variants_pred_fv_eq)

lemma (in stateful_protocol_model) timpl_closure_subst:
  assumes t: "wftrm t" "x  fv t. a. Γv x = TAtom (Atom a)"
    and δ: "wtsubst δ" "wftrms (subst_range δ)"
  shows "timpl_closure (t  δ) T = timpl_closure t T set δ"
proof
  have "s  timpl_closure t T set δ"
    when "s  timpl_closure (t  δ) T" for s
    using that
  proof (induction s rule: timpl_closure.induct)
    case FP thus ?case using timpl_closure.FP[of t T] by simp
  next
    case (TI u a b s)
    then obtain u' where u': "u'  timpl_closure t T" "u = u'  δ" by moura
    
    have u'_fv: "x  fv u'. a. Γv x = TAtom (Atom a)"
      using timpl_closure_fv_eq[OF u'(1)] t(2) by simp
    hence u_fv: "x  fv u. a. Γv x = TAtom (Atom a)"
      using u'(2) wt_subst_trm''[OF δ(1)] wt_subst_const_fv_type_eq[OF _ δ(1,2), of u']
      by fastforce

    have "x  fv u'  fv s. (y. δ x = Var y)  (f. δ x = Fun f []  Abs a  f)"
    proof (intro ballI)
      fix x assume x: "x  fv u'  fv s"
      then obtain c where c: "Γv x = TAtom (Atom c)"
        using u'_fv u_fv term_variants_pred_fv_eq[OF TI.hyps(3)]
        by blast

      show "(y. δ x = Var y)  (f. δ x = Fun f []  Abs a  f)"
      proof (cases "δ x")
        case (Fun f T)
        hence **: "Γ (Fun f T) = TAtom (Atom c)" and "wftrm (Fun f T)"
          using c wt_subst_trm''[OF δ(1), of "Var x"] δ(2)
          by fastforce+
        hence "δ x = Fun f []" using Fun const_type_inv_wf by metis
        thus ?thesis using ** by force
      qed metis
    qed
    hence *: "x  fv u'  fv s.
                (y. δ x = Var y)  (f. δ x = Fun f []  ((λ_. [])(Abs a := [Abs b])) f = [])"
      by fastforce

    obtain s' where s': "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u' s'" "s = s'  δ"
      using term_variants_pred_subst'[OF _ *] u'(2) TI.hyps(3)
      by blast

    show ?case using timpl_closure.TI[OF u'(1) TI.hyps(2) s'(1)] s'(2) by blast
  qed
  thus "timpl_closure (t  δ) T  timpl_closure t T set δ" by fast

  have "s  timpl_closure (t  δ) T"
    when s: "s  timpl_closure t T set δ" for s
  proof -
    obtain s' where s': "s'  timpl_closure t T" "s = s'  δ" using s by moura
    have "s'  δ  timpl_closure (t  δ) T" using s'(1)
    proof (induction s' rule: timpl_closure.induct)
      case FP thus ?case using timpl_closure.FP[of "t  δ" T] by simp
    next
      case (TI u' a b s') show ?case
        using timpl_closure.TI[OF TI.IH TI.hyps(2)]
              term_variants_pred_subst[OF TI.hyps(3)]
        by blast
    qed
    thus ?thesis using s'(2) by metis
  qed
  thus "timpl_closure t T set δ  timpl_closure (t  δ) T" by fast
qed

lemma (in stateful_protocol_model) timpl_closure_subst_subset:
  assumes t: "t  M"
    and M: "wftrms M" "x  fvset M. a. Γv x = TAtom (Atom a)"
    and δ: "wtsubst δ" "wftrms (subst_range δ)" "ground (subst_range δ)" "subst_domain δ  fvset M"
    and M_supset: "timpl_closure t T  M"
  shows "timpl_closure (t  δ) T  M set δ"
proof -
  have t': "wftrm t" "x  fv t. a. Γv x = TAtom (Atom a)" using t M by auto
  show ?thesis using timpl_closure_subst[OF t' δ(1,2), of T] M_supset by blast
qed

lemma (in stateful_protocol_model) timpl_closure_set_subst_subset:
  assumes M: "wftrms M" "x  fvset M. a. Γv x = TAtom (Atom a)"
    and δ: "wtsubst δ" "wftrms (subst_range δ)" "ground (subst_range δ)" "subst_domain δ  fvset M"
    and M_supset: "timpl_closure_set M T  M"
  shows "timpl_closure_set (M set δ) T  M set δ"
using timpl_closure_subst_subset[OF _ M δ, of _ T] M_supset
      timpl_closure_set_is_timpl_closure_union[of "M set δ" T]
      timpl_closure_set_is_timpl_closure_union[of M T]
by auto

lemma timpl_closure_set_Union:
  "timpl_closure_set (Ms) T = (M  Ms. timpl_closure_set M T)"
using timpl_closure_set_is_timpl_closure_union[of "Ms" T]
      timpl_closure_set_is_timpl_closure_union[of _ T]
by force

lemma timpl_closure_set_Union_subst_set:
  assumes "s  timpl_closure_set ({M set δ | δ. P δ}) T"
  shows "δ. P δ  s  timpl_closure_set (M set δ) T"
using assms timpl_closure_set_is_timpl_closure_union[of "({M set δ | δ. P δ})" T]
      timpl_closure_set_is_timpl_closure_union[of _ T]
by blast

lemma timpl_closure_set_Union_subst_singleton:
  assumes "s  timpl_closure_set {t  δ | δ. P δ} T"
  shows "δ. P δ  s  timpl_closure_set {t  δ} T"
using assms timpl_closure_set_is_timpl_closure_union[of "{t  δ |δ. P δ}" T]
      timpl_closureton_is_timpl_closure[of _ T]
by fast

lemma timpl_closure'_inv:
  assumes "(s, t)  timpl_closure' TI"
  shows "(x. s = Var x  t = Var x)  (f g S T. s = Fun f S  t = Fun g T  length S = length T)"
using assms unfolding timpl_closure'_def
proof (induction rule: rtrancl_induct)
  case base thus ?case by (cases s) auto
next
  case (step t u)
  obtain a b where ab: "(a, b)  TI" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) t u"
    using timpl_closure'_step_inv[OF step.hyps(2)] by blast
  show ?case using step.IH
  proof
    assume "x. s = Var x  t = Var x"
    thus ?case using step.hyps(2) term_variants_pred_inv_Var ab by fastforce
  next
    assume "f g S T. s = Fun f S  t = Fun g T  length S = length T"
    then obtain f g S T where st: "s = Fun f S" "t = Fun g T" "length S = length T" by moura
    thus ?case
      using ab step.hyps(2) term_variants_pred_inv'[of "(λ_. [])(Abs a := [Abs b])" g T u]
      by auto
  qed
qed

lemma timpl_closure'_inv':
  assumes "(s, t)  timpl_closure' TI"
  shows "(x. s = Var x  t = Var x) 
         (f g S T. s = Fun f S  t = Fun g T  length S = length T 
                    (i < length T. (S ! i, T ! i)  timpl_closure' TI) 
                    (f  g  is_Abs f  is_Abs g  (the_Abs f, the_Abs g)  TI+))"
    (is "?A s t  ?B s t (timpl_closure' TI)")
using assms unfolding timpl_closure'_def
proof (induction rule: rtrancl_induct)
  case base thus ?case by (cases s) auto
next
  case (step t u)
  obtain a b where ab: "(a, b)  TI" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) t u"
    using timpl_closure'_step_inv[OF step.hyps(2)] by blast
  show ?case using step.IH
  proof
    assume "?A s t"
    thus ?case using step.hyps(2) term_variants_pred_inv_Var ab by fastforce
  next
    assume "?B s t ((timpl_closure'_step TI)*)"
    then obtain f g S T where st:
        "s = Fun f S" "t = Fun g T" "length S = length T"
        "i. i < length T  (S ! i, T ! i)  (timpl_closure'_step TI)*"
        "f  g  is_Abs f  is_Abs g  (the_Abs f, the_Abs g)  TI+"
      by moura
    obtain h U where u:
        "u = Fun h U" "length T = length U"
        "i. i < length T  term_variants_pred ((λ_. [])(Abs a := [Abs b])) (T ! i) (U ! i)"
        "g  h  is_Abs g  is_Abs h  (the_Abs g, the_Abs h)  TI+"
      using ab(2) st(2) r_into_trancl[OF ab(1)]
            term_variants_pred_inv'(1,2,3,4)[of "(λ_. [])(Abs a := [Abs b])" g T u]
            term_variants_pred_inv'(5)[of "(λ_. [])(Abs a := [Abs b])" g T u "Abs a" "Abs b"]
      unfolding is_Abs_def the_Abs_def by force

    have "(S ! i, U ! i)  (timpl_closure'_step TI)*" when i: "i < length U" for i
      using u(2) i rtrancl.rtrancl_into_rtrancl[OF
              st(4)[of i] timpl_closure'_step.intros[OF ab(1) u(3)[of i]]]
      by argo
    moreover have "length S = length U" using st u by argo
    moreover have "is_Abs f  is_Abs h  (the_Abs f, the_Abs h)  TI+" when fh: "f  h"
      using fh st u by fastforce
    ultimately show ?case using st(1) u(1) by blast
  qed
qed

lemma timpl_closure'_inv'':
  assumes "(Fun f S, Fun g T)  timpl_closure' TI"
  shows "length S = length T"
    and "i. i < length T  (S ! i, T ! i)  timpl_closure' TI"
    and "f  g  is_Abs f  is_Abs g  (the_Abs f, the_Abs g)  TI+"
using assms timpl_closure'_inv' by auto

lemma timpl_closure_Fun_inv:
  assumes "s  timpl_closure (Fun f T) TI"
  shows "g S. s = Fun g S"
using assms timpl_closure_is_timpl_closure' timpl_closure'_inv
by fastforce

lemma timpl_closure_Fun_inv':
  assumes "Fun g S  timpl_closure (Fun f T) TI"
  shows "length S = length T"
    and "i. i < length S  S ! i  timpl_closure (T ! i) TI"
    and "f  g  is_Abs f  is_Abs g  (the_Abs f, the_Abs g)  TI+"
using assms timpl_closure_is_timpl_closure'
by (metis timpl_closure'_inv''(1), metis timpl_closure'_inv''(2), metis timpl_closure'_inv''(3))

lemma timpl_closure_Fun_not_Var[simp]:
  "Fun f T  timpl_closure (Var x) TI"
using timpl_closure_Var_inv by fast

lemma timpl_closure_Var_not_Fun[simp]:
  "Var x  timpl_closure (Fun f T) TI"
using timpl_closure_Fun_inv by fast

lemma (in stateful_protocol_model) timpl_closure_wf_trms:
  assumes m: "wftrm m"
  shows "wftrms (timpl_closure m TI)"
proof
  fix t assume "t  timpl_closure m TI"
  thus "wftrm t"
  proof (induction t rule: timpl_closure.induct)
    case TI thus ?case using term_variants_pred_wf_trms by force
  qed (rule m)
qed

lemma (in stateful_protocol_model) timpl_closure_set_wf_trms:
  assumes M: "wftrms M"
  shows "wftrms (timpl_closure_set M TI)"
proof
  fix t assume "t  timpl_closure_set M TI"
  then obtain m where "t  timpl_closure m TI" "m  M" "wftrm m"
    using M timpl_closure_set_is_timpl_closure_union by blast
  thus "wftrm t" using timpl_closure_wf_trms by blast
qed

lemma timpl_closure_Fu_inv:
  assumes "t  timpl_closure (Fun (Fu f) T) TI"
  shows "S. length S = length T  t = Fun (Fu f) S"
using assms
proof (induction t rule: timpl_closure.induct)
  case (TI u a b s)
  then obtain U where U: "length U = length T" "u = Fun (Fu f) U"
    by moura
  hence *: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) (Fun (Fu f) U) s"
    using TI.hyps(3) by meson

  show ?case
    using term_variants_pred_inv'(1,2,4)[OF *] U
    by force
qed simp

lemma timpl_closure_Fu_inv':
  assumes "Fun (Fu f) T  timpl_closure t TI"
  shows "S. length S = length T  t = Fun (Fu f) S"
using assms
proof (induction "Fun (Fu f) T" arbitrary: T rule: timpl_closure.induct)
  case (TI u a b)
  obtain g U where U:
      "u = Fun g U" "length U = length T"
      "Fu f  g  Abs a = g  Fu f = Abs b"
    using term_variants_pred_inv''[OF TI.hyps(4)] by fastforce

  have g: "g = Fu f" using U(3) by blast
  
  show ?case using TI.hyps(2)[OF U(1)[unfolded g]] U(2) by auto
qed simp

lemma timpl_closure_no_Abs_eq:
  assumes "t  timpl_closure s TI"
    and "f  funs_term t. ¬is_Abs f"
  shows "t = s"
using assms
proof (induction t rule: timpl_closure.induct)
  case (TI t a b s) thus ?case
    using term_variants_pred_eq_case_Abs[of a b t s]
    unfolding timpl_apply_term_def term_variants_pred_iff_in_term_variants[symmetric]
    by metis
qed simp

lemma timpl_closure_set_no_Abs_in_set:
  assumes "t  timpl_closure_set FP TI"
    and "f  funs_term t. ¬is_Abs f"
  shows "t  FP"
using assms timpl_closure_no_Abs_eq unfolding timpl_closure_set_def by blast

lemma timpl_closure_funs_term_subset:
  "(funs_term ` (timpl_closure t TI))  funs_term t  Abs ` snd ` TI"
  (is "?A  ?B  ?C")
proof
  fix f assume "f  ?A"
  then obtain s where "s  timpl_closure t TI" "f  funs_term s" by moura
  thus "f  ?B  ?C"
  proof (induction s rule: timpl_closure.induct)
    case (TI u a b s)
    have "Abs b  Abs ` snd ` TI" using TI.hyps(2) by force
    thus ?case using term_variants_pred_funs_term[OF TI.hyps(3) TI.prems] TI.IH by force
  qed blast
qed

lemma timpl_closure_set_funs_term_subset:
  "(funs_term ` (timpl_closure_set FP TI))  (funs_term ` FP)  Abs ` snd ` TI"
using timpl_closure_funs_term_subset[of _ TI]
      timpl_closure_set_is_timpl_closure_union[of FP TI]
by auto

lemma funs_term_OCC_TI_subset:
  defines "absc  λa. Fun (Abs a) []"
  assumes OCC1: "t  FP. f  funs_term t. is_Abs f  f  Abs ` OCC"
    and OCC2: "snd ` TI  OCC"
  shows "t  timpl_closure_set FP TI. f  funs_term t. is_Abs f  f  Abs ` OCC" (is ?A)
    and "t  absc ` OCC. (a,b)  TI. s  set a --» b⟩⟨t. s  absc ` OCC" (is ?B)
proof -
  let ?F = "(funs_term ` FP)"
  let ?G = "Abs ` snd ` TI"

  show ?A
  proof (intro ballI impI)
    fix t f assume t: "t  timpl_closure_set FP TI" and f: "f  funs_term t" "is_Abs f"
    hence "f  ?F  f  ?G" using timpl_closure_set_funs_term_subset[of FP TI] by auto
    thus "f  Abs ` OCC"
    proof
      assume "f  ?F" thus ?thesis using OCC1 f(2) by fast
    next
      assume "f  ?G" thus ?thesis using OCC2 by auto
    qed
  qed

  { fix s t a b
    assume t: "t  absc ` OCC"
      and ab: "(a, b)  TI"
      and s: "s  set a --» b⟩⟨t"
    obtain c where c: "t = absc c" "c  OCC" using t by moura
    hence "s = absc b  s = absc c"
      using ab s timpl_apply_const'[of c a b] unfolding absc_def by auto
    moreover have "b  OCC" using ab OCC2 by auto
    ultimately have "s  absc ` OCC" using c(2) by blast
  } thus ?B by blast
qed

lemma (in stateful_protocol_model) intruder_synth_timpl_closure_set:
  fixes M::"('fun,'atom,'sets,'lbl) prot_terms" and t::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "M c t"
    and "s  timpl_closure t TI"
  shows "timpl_closure_set M TI c s"
using assms
proof (induction t arbitrary: s rule: intruder_synth_induct)
  case (AxiomC t)
  hence "s  timpl_closure_set M TI"
    using timpl_closure_set_is_timpl_closure_union[of M TI]
    by blast
  thus ?case by simp
next
  case (ComposeC T f)
  obtain g S where s: "s = Fun g S"
    using timpl_closure_Fun_inv[OF ComposeC.prems] by moura
  hence s':
      "f = g" "length S = length T"
      "i. i < length S  S ! i  timpl_closure (T ! i) TI"
    using timpl_closure_Fun_inv'[of g S f T TI] ComposeC.prems ComposeC.hyps(2)
    unfolding is_Abs_def by fastforce+
  
  have "timpl_closure_set M TI c u" when u: "u  set S" for u
    using ComposeC.IH u s'(2,3) in_set_conv_nth[of _ T] in_set_conv_nth[of u S] by auto
  thus ?case
    using s s'(1,2) ComposeC.hyps(1,2) intruder_synth.ComposeC[of S g "timpl_closure_set M TI"]
    by argo
qed

lemma (in stateful_protocol_model) intruder_synth_timpl_closure':
  fixes M::"('fun,'atom,'sets,'lbl) prot_terms" and t::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "timpl_closure_set M TI c t"
    and "s  timpl_closure t TI"
  shows "timpl_closure_set M TI c s"
by (metis intruder_synth_timpl_closure_set[OF assms] timpl_closure_set_idem)

lemma timpl_closure_set_absc_subset_in:
  defines "absc  λa. Fun (Abs a) []"
  assumes A: "timpl_closure_set (absc ` A) TI  absc ` A"
    and a: "a  A" "(a,b)  TI+"
  shows "b  A"
proof -
  have "timpl_closure (absc a) (TI+)  absc ` A"
    using a(1) A timpl_closure_timpls_trancl_eq
    unfolding timpl_closure_set_def by fast
  thus ?thesis
    using timpl_closure.TI[OF timpl_closure.FP[of "absc a"] a(2), of "absc b"]
          term_variants_P[of "[]" "[]" "(λ_. [])(Abs a := [Abs b])" "Abs b" "Abs a"]
    unfolding absc_def by auto
qed

lemma timpl_closure_Abs_ex:
  assumes t: "s  timpl_closure t TI"
    and a: "Abs a  funs_term t"
  shows "b ts. (a,b)  TI*  Fun (Abs b) ts  s"
using t
proof (induction rule: timpl_closure.induct)
  case (TI u b c s)
  obtain d ts where d: "(a,d)  TI*" "Fun (Abs d) ts  u" using TI.IH by blast
  note 0 = TI.hyps(2) d(1) term_variants_pred_inv'(5)[OF term_variants_pred_const]
  show ?case using TI.hyps(3) d(2)
  proof (induction rule: term_variants_pred.induct)
    case (term_variants_P T S g f)
    note hyps = term_variants_P.hyps
    note prems = term_variants_P.prems
    note IH = term_variants_P.IH
    show ?case
    proof (cases "Fun (Abs d) ts = Fun f T")
      case False
      hence "t  set T. Fun (Abs d) ts  t" using prems(1) by force
      then obtain i where i: "i < length T" "Fun (Abs d) ts  T ! i" by (metis in_set_conv_nth)
      show ?thesis by (metis IH[OF i] i(1) hyps(1) nth_mem subtermeqI'' term.order.trans)
    qed (metis hyps(3) 0 prot_fun.sel(4) r_into_rtrancl rtrancl_trans term.eq_refl term.sel(2))
  next
    case (term_variants_Fun T S f)
    note hyps = term_variants_Fun.hyps
    note prems = term_variants_Fun.prems
    note IH = term_variants_Fun.IH
    show ?case
    proof (cases "Fun (Abs d) ts = Fun f T")
      case False
      hence "t  set T. Fun (Abs d) ts  t" using prems(1) by force
      then obtain i where i: "i < length T" "Fun (Abs d) ts  T ! i" by (metis in_set_conv_nth)
      show ?thesis by (metis IH[OF i] i(1) hyps(1) nth_mem subtermeqI'' term.order.trans)
    qed (metis 0(2) term.eq_refl term.sel(2))
  qed simp
qed (meson a funs_term_Fun_subterm rtrancl_eq_or_trancl)

lemma timpl_closure_trans:
  assumes "s  timpl_closure t TI"
    and "u  timpl_closure s TI"
  shows "u  timpl_closure t TI"
using assms unfolding timpl_closure_is_timpl_closure' timpl_closure'_def by simp

lemma (in stateful_protocol_model) term_variants_pred_Anaf_keys:
  assumes
    "length ss = length ts"
    "x  fv k. x < length ss"
    "i. i < length ss  term_variants_pred P (ss ! i) (ts ! i)"
  shows "term_variants_pred P (k  (!) ss) (k  (!) ts)"
using assms by (meson term_variants_pred_subst'')

lemma (in stateful_protocol_model) term_variants_pred_Ana_keys:
  fixes a b and s t::"('fun,'atom,'sets,'lbl) prot_term"
  defines "P  ((λ_. [])(Abs a := [Abs b]))"
  assumes ab: "term_variants_pred P s t"
    and s: "Ana s = (Ks, Rs)"
    and t: "Ana t = (Kt, Rt)"
  shows "length Kt = length Ks" (is ?A)
    and "i < length Ks. term_variants_pred P (Ks ! i) (Kt ! i)" (is ?B)
proof -
  have ?A ?B when "s = Var x" for x
    using that ab s t iffD1[OF term_variants_pred_inv_Var(1) ab[unfolded that]] by auto
  moreover have ?A ?B when s': "s = Fun f ss" for f ss
  proof -
    obtain g ts where t':
        "t = Fun g ts" "length ss = length ts"
        "i. i < length ss  term_variants_pred P (ss ! i) (ts ! i)"
        "f  g  f = Abs a  g = Abs b"
      using term_variants_pred_inv'[OF ab[unfolded s']]
      unfolding P_def by fastforce
    have ?A ?B when "f  g" using that s s' t t'(1,2,4) by auto
    moreover have A: ?A when fg: "f = g"
      using s t Ana_Fu_keys_length_eq[OF t'(2)] Ana_nonempty_inv[of s] Ana_nonempty_inv[of t]
      unfolding fg s' t'(1) by (metis (no_types) fst_conv term.inject(2))
    moreover have ?B when fg: "f = g"
    proof (cases "Ana s = ([],[])")
      case True thus ?thesis using s t t'(2,3) A[OF fg] unfolding fg s' t'(1) by auto
    next
      case False
      then obtain h Kh Rh where h:
          "f = Fu h" "g = Fu h" "arityf h = length ss" "arityf h > 0" "Anaf h = (Kh, Rh)"
          "Ana s = (Kh list (!) ss, map ((!) ss) Rh)" "Ana t = (Kh list (!) ts, map ((!) ts) Rh)"
        using A[OF fg] s t t'(2,3) Ana_nonempty_inv[of s] Ana_nonempty_inv[of t]
        unfolding fg s' t'(1) by fastforce
      show ?thesis
      proof (intro allI impI)
        fix i assume i: "i < length Ks"
        have Ks: "Ks = Kh list (!) ss" and Kt: "Kt = Kh list (!) ts"
          using h(6,7) s t by auto

        have 0: "Kh ! i  set Kh" using Ks i by simp

        have 1: "x  fv (Kh ! i). x < length ss"
          using 0 Anaf_assm2_alt[OF h(5)]
          unfolding h(1-3) by fastforce

        have "term_variants_pred P (Kh ! i  (!) ss) (Kh ! i  (!) ts)"
          using term_variants_pred_Anaf_keys[OF t'(2) 1 t'(3)]
          unfolding P_def by fast
        thus "term_variants_pred P (Ks ! i) (Kt ! i)"
          using i unfolding Ks Kt by simp
      qed
    qed
    ultimately show ?A ?B by fast+
  qed
  ultimately show ?A ?B by (cases s; simp_all)+
qed

lemma (in stateful_protocol_model) timpl_closure_Ana_keys:
  fixes s t::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "t  timpl_closure s TI"
    and "Ana s = (Ks, Rs)"
    and "Ana t = (Kt, Rt)"
  shows "length Kt = length Ks" (is ?A)
    and "i < length Ks. Kt ! i  timpl_closure (Ks ! i) TI" (is ?B)
using assms
proof (induction arbitrary: Ks Rs Kt Rt rule: timpl_closure.induct)
  case FP
  { case 1 thus ?case by simp }
  { case 2 thus ?case using FP timpl_closure.FP by force }
next
  case (TI u a b t)
  obtain Ku Ru where u: "Ana u = (Ku, Ru)" by (metis surj_pair)
  note 0 = term_variants_pred_Ana_keys[OF TI.hyps(3) u]
  { case 1 thus ?case using 0(1) TI.IH(1) u by fastforce }
  { case 2 thus ?case by (metis 0(2)[OF 2(2)] TI.IH[OF 2(1) u] timpl_closure.TI[OF _ TI.hyps(2)]) }
qed

lemma (in stateful_protocol_model) timpl_closure_Ana_keys_length_eq:
  fixes s t::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "t  timpl_closure s TI"
    and "Ana s = (Ks, Rs)"
    and "Ana t = (Kt, Rt)"
  shows "length Kt = length Ks"
by (rule timpl_closure_Ana_keys(1,2)[OF assms])

lemma (in stateful_protocol_model) timpl_closure_Ana_keys_subset:
  fixes s t::"('fun,'atom,'sets,'lbl) prot_term"
  assumes "t  timpl_closure s TI"
    and "Ana s = (Ks, Rs)"
    and "Ana t = (Kt, Rt)"
  shows "set Kt  timpl_closure_set (set Ks) TI"
proof -
  note 0 = timpl_closure_Ana_keys[OF assms]
  have "i < length Ks. Kt ! i  timpl_closure_set (set Ks) TI"
    using in_set_conv_nth 0(2) unfolding timpl_closure_set_def by auto
  thus "set Kt  timpl_closure_set (set Ks) TI"
    using 0(1) by (metis subsetI in_set_conv_nth)
qed


subsection ‹Composition-only Intruder Deduction Modulo Term Implication Closure of the Intruder Knowledge›
context stateful_protocol_model
begin

fun in_trancl where
  "in_trancl TI a b = (
    if (a,b)  set TI then True
    else list_ex (λ(c,d). c = a  in_trancl (removeAll (c,d) TI) d b) TI)"

definition in_rtrancl where
  "in_rtrancl TI a b  a = b  in_trancl TI a b"

declare in_trancl.simps[simp del]

fun timpls_transformable_to where
  "timpls_transformable_to TI (Var x) (Var y) = (x = y)"
| "timpls_transformable_to TI (Fun f T) (Fun g S) = (
    (f = g  (is_Abs f  is_Abs g  (the_Abs f, the_Abs g)  set TI)) 
    list_all2 (timpls_transformable_to TI) T S)"
| "timpls_transformable_to _ _ _ = False"

fun timpls_transformable_to' where
  "timpls_transformable_to' TI (Var x) (Var y) = (x = y)"
| "timpls_transformable_to' TI (Fun f T) (Fun g S) = (
    (f = g  (is_Abs f  is_Abs g  in_trancl TI (the_Abs f) (the_Abs g))) 
    list_all2 (timpls_transformable_to' TI) T S)"
| "timpls_transformable_to' _ _ _ = False"

fun equal_mod_timpls where
  "equal_mod_timpls TI (Var x) (Var y) = (x = y)"
| "equal_mod_timpls TI (Fun f T) (Fun g S) = (
    (f = g  (is_Abs f  is_Abs g 
                ((the_Abs f, the_Abs g)  set TI 
                 (the_Abs g, the_Abs f)  set TI 
                 (ti  set TI. (the_Abs f, snd ti)  set TI  (the_Abs g, snd ti)  set TI)))) 
    list_all2 (equal_mod_timpls TI) T S)"
| "equal_mod_timpls _ _ _ = False"

fun intruder_synth_mod_timpls where
  "intruder_synth_mod_timpls M TI (Var x) = List.member M (Var x)"
| "intruder_synth_mod_timpls M TI (Fun f T) = (
    (list_ex (λt. timpls_transformable_to TI t (Fun f T)) M) 
    (public f  length T = arity f  list_all (intruder_synth_mod_timpls M TI) T))"

fun intruder_synth_mod_timpls' where
  "intruder_synth_mod_timpls' M TI (Var x) = List.member M (Var x)"
| "intruder_synth_mod_timpls' M TI (Fun f T) = (
    (list_ex (λt. timpls_transformable_to' TI t (Fun f T)) M) 
    (public f  length T = arity f  list_all (intruder_synth_mod_timpls' M TI) T))"

fun intruder_synth_mod_eq_timpls where
  "intruder_synth_mod_eq_timpls M TI (Var x) = (Var x  M)"
| "intruder_synth_mod_eq_timpls M TI (Fun f T) = (
    (t  M. equal_mod_timpls TI t (Fun f T)) 
    (public f  length T = arity f  list_all (intruder_synth_mod_eq_timpls M TI) T))"

definition analyzed_closed_mod_timpls where
  "analyzed_closed_mod_timpls M TI 
    let ti = intruder_synth_mod_timpls M TI;
        cl = λts. comp_timpl_closure ts (set TI);
        f = list_all ti;
        g = λt. if f (fst (Ana t)) then f (snd (Ana t))
                else if list_all (λt. f  funs_term t. ¬is_Abs f) (fst (Ana t)) then True
                else if s  cl (set (fst (Ana t))). ¬ti s then True
                else s  cl {t}. case Ana s of (K,R)  f K  f R
    in list_all g M"

definition analyzed_closed_mod_timpls' where
  "analyzed_closed_mod_timpls' M TI 
    let f = list_all (intruder_synth_mod_timpls' M TI);
        g = λt. if f (fst (Ana t)) then f (snd (Ana t))
                else if list_all (λt. f  funs_term t. ¬is_Abs f) (fst (Ana t)) then True
                else s  comp_timpl_closure {t} (set TI). case Ana s of (K,R)  f K  f R
    in list_all g M"

lemma term_variants_pred_Abs_Ana_keys:
  fixes a b
  defines "P  ((λ_. [])(Abs a := [Abs b]))"
  assumes st: "term_variants_pred P s t"
  shows "length (fst (Ana s)) = length (fst (Ana t))" (is "?P s t")
    and "i < length (fst (Ana s)). term_variants_pred P (fst (Ana s) ! i) (fst (Ana t) ! i)"
          (is "?Q s t")
proof -
  show "?P s t" using st
  proof (induction s t rule: term_variants_pred.induct)
    case (term_variants_Fun T S f) show ?case
    proof (cases f)
      case (Fu g) thus ?thesis using term_variants_Fun Ana_Fu_keys_length_eq by blast
    qed simp_all
  qed (simp_all add: P_def)

  show "?Q s t" using st
  proof (induction s t rule: term_variants_pred.induct)
    case (term_variants_Fun T S f)
    note hyps = term_variants_Fun.hyps
    let ?K = "λU. fst (Ana (Fun f U))"

    show ?case
    proof (cases f)
      case (Fu g) show ?thesis
      proof (cases "arityf g = length T  arityf g > 0")
        case True
        hence *: "?K T = fst (Anaf g) list (!) T"
                 "?K S = fst (Anaf g) list (!) S"
          using Fu Ana_Fu_intro fst_conv prod.collapse
          by (metis (mono_tags, lifting), metis (mono_tags, lifting) hyps(1))

        have K: "j < length T" when j: "j  fvset (set (fst (Anaf g)))" for j
          using True Anaf_assm2_alt[of g "fst (Anaf g)" _ j ]
          by (metis UnI1 prod.collapse that) 

        show ?thesis
        proof (intro allI impI)
          fix i assume i: "i < length (?K T)"
          let ?u = "fst (Anaf g) ! i"

          have **: "?K T ! i = ?u  (!) T" "?K S ! i = ?u  (!) S"
            using * i by simp_all

          have ***: "x < length T" when "x  fv (fst (Anaf g) ! i)" for x
            using that K Anaf_assm2_alt[of g "fst (Anaf g)" _ x] i hyps(1)
            unfolding * by force

          show "term_variants_pred P (?K T ! i) (?K S ! i)"
            using i hyps K *** term_variants_pred_subst''[of ?u P "(!) T" "(!) S"]
            unfolding * by auto
        qed
      qed (auto simp add: Fu)
    qed simp_all
  qed (simp_all add: P_def)
qed

lemma term_variants_pred_Abs_eq_case:
  assumes t: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) s t" (is "?R s t")
    and s: "f  funs_term s. ¬is_Abs f" (is "?P s")
  shows "s = t"
using s term_variants_pred_eq_case[OF t] by fastforce

lemma term_variants_Ana_keys_no_Abs_eq_case:
  fixes s t::"(('fun,'atom,'sets,'lbl) prot_fun,'v) term"
  assumes t: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) s t" (is "?R s t")
    and s: "t  set (fst (Ana s)). f  funs_term t. ¬is_Abs f" (is "?P s")
  shows "fst (Ana t) = fst (Ana s)" (is "?Q t s")
using s term_variants_pred_Abs_Ana_keys[OF t] term_variants_pred_Abs_eq_case[of a b]
by (metis nth_equalityI nth_mem)

lemma timpl_closure_Ana_keys_no_Abs_eq_case:
  assumes t: "t  timpl_closure s TI"
    and s: "t  set (fst (Ana s)). f  funs_term t