Theory Typed_Model

(*  Title:      Typed_Model.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹The Typed Model›
theory Typed_Model
imports Lazy_Intruder
begin

text ‹Term types›
type_synonym ('f,'v) term_type = "('f,'v) term"

text ‹Constructors for term types›
abbreviation (input) TAtom::"'v  ('f,'v) term_type" where
  "TAtom a  Var a"

abbreviation (input) TComp::"['f, ('f,'v) term_type list]  ('f,'v) term_type" where
  "TComp f ts  Fun f ts"


text ‹
  The typed model extends the intruder model with a typing function Γ› that assigns types to terms.
›
locale typed_model = intruder_model arity public Ana
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,'var) term  (('fun,'var) term list × ('fun,'var) term list)"
  +
  fixes Γ::"('fun,'var) term  ('fun,'atom::finite) term_type"
  assumes const_type: "c. arity c = 0  a. ts. Γ (Fun c ts) = TAtom a"
    and fun_type: "f ts. arity f > 0  Γ (Fun f ts) = TComp f (map Γ ts)"
    and Γ_wf: "x f ts. TComp f ts  Γ (Var x)  arity f > 0"
              "x. wftrm (Γ (Var x))"
begin


subsection ‹Definitions›
text ‹The set of atomic types›
abbreviation "𝔗a  UNIV::('atom set)"

text ‹Well-typed substitutions›
definition wtsubst where
  "wtsubst σ  (v. Γ (Var v) = Γ (σ v))"

text ‹The set of sub-message patterns (SMP)›
inductive_set SMP::"('fun,'var) terms  ('fun,'var) terms" for M where
  MP[intro]: "t  M  t  SMP M"
| Subterm[intro]: "t  SMP M; t'  t  t'  SMP M"
| Substitution[intro]: "t  SMP M; wtsubst δ; wftrms (subst_range δ)  (t  δ)  SMP M"
| Ana[intro]: "t  SMP M; Ana t = (K,T); k  set K  k  SMP M"

text ‹
  Type-flaw resistance for sets:
  Unifiable sub-message patterns must have the same type (unless they are variables)
›
definition tfrset where
  "tfrset M  (s  SMP M - (Var`𝒱). t  SMP M - (Var`𝒱). (δ. Unifier δ s t)  Γ s = Γ t)"

text ‹
  Type-flaw resistance for strand steps:
  - The terms in a satisfiable equality step must have the same types
  - Inequality steps must satisfy the conditions of the "inequality lemma"›
fun tfrstp where
  "tfrstp (Equality a t t') = ((δ. Unifier δ t t')  Γ t = Γ t')"
| "tfrstp (Inequality X F) = (
      (x  fvpairs F - set X. a. Γ (Var x) = TAtom a) 
      (f T. Fun f T  subtermsset (trmspairs F)  T = []  (s  set T. s  Var ` set X)))"
| "tfrstp _ = True"

text ‹
  Type-flaw resistance for strands:
  - The set of terms in strands must be type-flaw resistant
  - The steps of strands must be type-flaw resistant
›
definition tfrst where
  "tfrst S  tfrset (trmsst S)  list_all tfrstp S"


subsection ‹Small Lemmata›
lemma tfrstp_list_all_alt_def:
  "list_all tfrstp S 
    ((a t t'. Equality a t t'  set S  (δ. Unifier δ t t')  Γ t = Γ t') 
    (X F. Inequality X F  set S  
      (x  fvpairs F - set X. a. Γ (Var x) = TAtom a)
     (f T. Fun f T  subtermsset (trmspairs F)  T = []  (s  set T. s  Var ` set X))))"
  (is "?P S  ?Q S")
proof
  show "?P S  ?Q S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp

  show "?Q S  ?P S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp
qed

lemma Γ_wf'': "TComp f T  Γ t  arity f > 0"
proof (induction t)
  case (Var x) thus ?case using Γ_wf(1)[of f T x] by blast
next
  case (Fun g S) thus ?case
    using fun_type[of g S] const_type[of g] by (cases "arity g") auto
qed

lemma Γ_wf': "wftrm t  wftrm (Γ t)"
proof (induction t)
  case (Fun f T)
  hence *: "arity f = length T" "t. t  set T  wftrm (Γ t)" unfolding wftrm_def by auto
  { assume "arity f = 0" hence ?case using const_type[of f] by auto }
  moreover
  { assume "arity f > 0" hence ?case using fun_type[of f] * by force }
  ultimately show ?case by auto 
qed (metis Γ_wf(2))

lemma fun_type_inv: assumes "Γ t = TComp f T" shows "arity f > 0"
using Γ_wf''(1)[of f T t] assms by simp_all

lemma fun_type_inv_wf: assumes "Γ t = TComp f T" "wftrm t" shows "arity f = length T"
using Γ_wf'[OF assms(2)] assms(1) unfolding wftrm_def by auto

lemma const_type_inv: "Γ (Fun c X) = TAtom a  arity c = 0"
by (rule ccontr, simp add: fun_type)

lemma const_type_inv_wf: assumes "Γ (Fun c X) = TAtom a" and "wftrm (Fun c X)" shows "X = []"
by (metis assms const_type_inv length_0_conv subtermeqI' wftrm_def)

lemma const_type': "c  𝒞. a  𝔗a. X. Γ (Fun c X) = TAtom a" using const_type by simp
lemma fun_type': "f  Σf. X. Γ (Fun f X) = TComp f (map Γ X)" using fun_type by simp

lemma fun_type_id_eq: "Γ (Fun f X) = TComp g Y  f = g"
by (metis const_type fun_type neq0_conv "term.inject"(2) "term.simps"(4))

lemma fun_type_length_eq: "Γ (Fun f X) = TComp g Y  length X = length Y"
by (metis fun_type fun_type_id_eq fun_type_inv(1) length_map term.inject(2))

lemma pgwt_type_map: 
  assumes "public_ground_wf_term t"
  shows "Γ t = TAtom a  f. t = Fun f []" "Γ t = TComp g Y  X. t = Fun g X  map Γ X = Y"
proof -
  let ?A = "Γ t = TAtom a  (f. t = Fun f [])"
  let ?B = "Γ t = TComp g Y  (X. t = Fun g X  map Γ X = Y)"
  have "?A  ?B"
  proof (cases "Γ t")
    case (Var a)
    obtain f X where "t = Fun f X" "arity f = length X"
      using pgwt_fun[OF assms(1)] pgwt_arity[OF assms(1)] by fastforce+
    thus ?thesis using const_type_inv Γ t = TAtom a by auto
  next
    case (Fun g Y)
    obtain f X where *: "t = Fun f X" using pgwt_fun[OF assms(1)] by force
    hence "f = g" "map Γ X = Y"
      using fun_type_id_eq Γ t = TComp g Y fun_type[OF fun_type_inv(1)[OF Γ t = TComp g Y]]
      by fastforce+
    thus ?thesis using *(1) Γ t = TComp g Y by auto 
  qed
  thus "Γ t = TAtom a  f. t = Fun f []" "Γ t = TComp g Y  X. t = Fun g X  map Γ X = Y"
    by auto
qed 

lemma wt_subst_Var[simp]: "wtsubst Var" by (metis wtsubst_def)

lemma wt_subst_trm: "(v. v  fv t  Γ (Var v) = Γ (θ v))  Γ t = Γ (t  θ)"
proof (induction t)
  case (Fun f X)
  hence *: "x. x  set X  Γ x = Γ (x  θ)" by auto
  show ?case
  proof (cases "f  Σf")
    case True
    hence "X. Γ (Fun f X) = TComp f (map Γ X)" using fun_type' by auto
    thus ?thesis using * by auto
  next
    case False
    hence "a  𝔗a. X. Γ (Fun f X) = TAtom a" using const_type' by auto
    thus ?thesis by auto
  qed
qed auto

lemma wt_subst_trm': "wtsubst σ; Γ s = Γ t  Γ (s  σ) = Γ (t  σ)"
by (metis wt_subst_trm wtsubst_def)

lemma wt_subst_trm'': "wtsubst σ  Γ t = Γ (t  σ)"
by (metis wt_subst_trm wtsubst_def)

lemma wt_subst_compose:
  assumes "wtsubst θ" "wtsubst δ" shows "wtsubst (θ s δ)"
proof -
  have "v. Γ (θ v) = Γ (θ v  δ)" using wt_subst_trm wtsubst δ unfolding wtsubst_def by metis
  moreover have "v. Γ (Var v) = Γ (θ v)" using wtsubst θ unfolding wtsubst_def by metis
  ultimately have "v. Γ (Var v) = Γ (θ v  δ)" by metis
  thus ?thesis unfolding wtsubst_def subst_compose_def by metis
qed

lemma wt_subst_TAtom_Var_cases:
  assumes θ: "wtsubst θ" "wftrms (subst_range θ)"
  and x: "Γ (Var x) = TAtom a"
  shows "(y. θ x = Var y)  (c. θ x = Fun c [])"
proof (cases "(y. θ x = Var y)")
  case False
  then obtain c T where c: "θ x = Fun c T"
    by (cases "θ x") simp_all
  hence "wftrm (Fun c T)"
    using θ(2) by fastforce
  hence "T = []"
    using const_type_inv_wf[of c T a] x c wt_subst_trm''[OF θ(1), of "Var x"]
    by fastforce
  thus ?thesis
    using c by blast
qed simp

lemma wt_subst_TAtom_fv:
  assumes θ: "wtsubst θ" "x. wftrm (θ x)"
  and "x  fv t - X. a. Γ (Var x) = TAtom a"
  shows "x  fv (t  θ) - fvset (θ ` X). a. Γ (Var x) = TAtom a"
using assms(3)
proof (induction t)
  case (Var x) thus ?case
  proof (cases "x  X")
    case False
    with Var obtain a where "Γ (Var x) = TAtom a" by atomize_elim auto
    hence *: "Γ (θ x) = TAtom a" "wftrm (θ x)" using θ unfolding wtsubst_def by auto
    show ?thesis
    proof (cases "θ x")
      case (Var y) thus ?thesis using * by auto
    next
      case (Fun f T)
      hence "T = []" using * const_type_inv[of f T a] unfolding wftrm_def by auto
      thus ?thesis using Fun by auto
    qed
  qed auto
qed fastforce

lemma wt_subst_TAtom_subterms_subst:
  assumes "wtsubst θ" "x  fv t. a. Γ (Var x) = TAtom a" "wftrms (θ ` fv t)"
  shows "subterms (t  θ) = subterms t set θ"
using assms(2,3)
proof (induction t)
  case (Var x)
  obtain a where a: "Γ (Var x) = TAtom a" using Var.prems(1) by atomize_elim auto
  hence "Γ (θ x) = TAtom a" using wt_subst_trm''[OF assms(1), of "Var x"] by simp
  hence "(y. θ x = Var y)  (c. θ x = Fun c [])"
    using const_type_inv_wf Var.prems(2) by (cases "θ x") auto
  thus ?case by auto
next
  case (Fun f T)
  have "subterms (t  θ) = subterms t set θ" when "t  set T" for t
    using that Fun.prems(1,2) Fun.IH[OF that]
    by auto
  thus ?case by auto
qed

lemma wt_subst_TAtom_subterms_set_subst: 
  assumes "wtsubst θ" "x  fvset M. a. Γ (Var x) = TAtom a" "wftrms (θ ` fvset M)"
  shows "subtermsset (M set θ) = subtermsset M set θ"
proof
  show "subtermsset (M set θ)  subtermsset M set θ"
  proof
    fix t assume "t  subtermsset (M set θ)"
    then obtain s where s: "s  M" "t  subterms (s  θ)" by auto
    thus "t  subtermsset M set θ"
      using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
      by auto
  qed

  show "subtermsset M set θ  subtermsset (M set θ)"
  proof
    fix t assume "t  subtermsset M set θ"
    then obtain s where s: "s  M" "t  subterms s set θ" by auto
    thus "t  subtermsset (M set θ)"
      using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
      by auto
  qed
qed

lemma wt_subst_subst_upd:
  assumes "wtsubst θ"
    and "Γ (Var x) = Γ t"
  shows "wtsubst (θ(x := t))"
using assms unfolding wtsubst_def
by (metis fun_upd_other fun_upd_same)

lemma wt_subst_const_fv_type_eq:
  assumes "x  fv t. a. Γ (Var x) = TAtom a"
    and δ: "wtsubst δ" "wftrms (subst_range δ)"
  shows "x  fv (t  δ). y  fv t. Γ (Var x) = Γ (Var y)"
using assms(1)
proof (induction t)
  case (Var x)
  then obtain a where a: "Γ (Var x) = TAtom a" by atomize_elim auto
  show ?case
  proof (cases "δ x")
    case (Fun f T)
    hence "wftrm (Fun f T)" "Γ (Fun f T) = TAtom a"
      using a wt_subst_trm''[OF δ(1), of "Var x"] δ(2) by fastforce+
    thus ?thesis using const_type_inv_wf Fun by fastforce
  qed (use a wt_subst_trm''[OF δ(1), of "Var x"] in simp)
qed fastforce

lemma TComp_term_cases:
  assumes "wftrm t" "Γ t = TComp f T"
  shows "(v. t = Var v)  (T'. t = Fun f T'  T = map Γ T'  T'  [])"
proof (cases "v. t = Var v")
  case False
  then obtain T' where T': "t = Fun f T'" "T = map Γ T'"
    using assms fun_type[OF fun_type_inv(1)[OF assms(2)]] fun_type_id_eq
    by (cases t) force+
  thus ?thesis using assms fun_type_inv(1) fun_type_inv_wf by fastforce
qed metis

lemma TAtom_term_cases:
  assumes "wftrm t" "Γ t = TAtom τ"
  shows "(v. t = Var v)  (f. t = Fun f [])"
using assms const_type_inv unfolding wftrm_def by (cases t) auto

lemma subtermeq_imp_subtermtypeeq:
  assumes "wftrm t" "s  t"
  shows "Γ s  Γ t"
using assms(2,1)
proof (induction t)
  case (Fun f T) thus ?case
  proof (cases "s = Fun f T")
    case False
    then obtain x where x: "x  set T" "s  x" using Fun.prems(1) by auto
    hence "wftrm x" using wf_trm_subtermeq[OF Fun.prems(2)] Fun_param_is_subterm[of _ T f] by auto
    hence "Γ s  Γ x" using Fun.IH[OF x] by simp
    moreover have "arity f > 0" using x fun_type_inv_wf Fun.prems
      by (metis length_pos_if_in_set term.order_refl wftrm_def)
    ultimately show ?thesis using x Fun.prems fun_type[of f T] by auto
  qed simp
qed simp

lemma subterm_funs_term_in_type:
  assumes "wftrm t" "Fun f T  t" "Γ (Fun f T) = TComp f (map Γ T)"
  shows "f  funs_term (Γ t)"
using assms(2,1,3)
proof (induction t)
  case (Fun f' T')
  hence [simp]: "wftrm (Fun f T)" by (metis wf_trm_subtermeq)
  { fix a assume τ: "Γ (Fun f' T') = TAtom a"
    hence "Fun f T = Fun f' T'" using Fun TAtom_term_cases subtermeq_Var_const by metis
    hence False using Fun.prems(3) τ by simp
  }
  moreover
  { fix g S assume τ: "Γ (Fun f' T') = TComp g S"
    hence "g = f'" "S = map Γ T'"
      using Fun.prems(2) fun_type_id_eq[OF τ] fun_type[OF fun_type_inv(1)[OF τ]]
      by auto
    hence τ': "Γ (Fun f' T') = TComp f' (map Γ T')" using τ by auto
    hence "g  funs_term (Γ (Fun f' T'))" using τ by auto
    moreover {
      assume "Fun f T  Fun f' T'"
      then obtain x where "x  set T'" "Fun f T  x" using Fun.prems(1) by auto
      hence "f  funs_term (Γ x)"
        using Fun.IH[OF _ _ _ Fun.prems(3), of x] wf_trm_subtermeq[OF wftrm (Fun f' T'), of x]
        by force
      moreover have "Γ x  set (map Γ T')" using τ' x  set T' by auto
      ultimately have "f  funs_term (Γ (Fun f' T'))" using τ' by auto
    }
    ultimately have ?case by (cases "Fun f T = Fun f' T'") (auto simp add: g = f')
  }
  ultimately show ?case by (cases "Γ (Fun f' T')") auto
qed simp

lemma wt_subst_fv_termtype_subterm:
  assumes "x  fv (θ y)"
    and "wtsubst θ"
    and "wftrm (θ y)"
  shows "Γ (Var x)  Γ (Var y)"
using subtermeq_imp_subtermtypeeq[OF assms(3) var_is_subterm[OF assms(1)]]
      wt_subst_trm''[OF assms(2), of "Var y"]
by auto

lemma wt_subst_fvset_termtype_subterm:
  assumes "x  fvset (θ ` Y)"
    and "wtsubst θ"
    and "wftrms (subst_range θ)"
  shows "y  Y. Γ (Var x)  Γ (Var y)"
using wt_subst_fv_termtype_subterm[OF _ assms(2), of x] assms(1,3)
by fastforce

lemma funs_term_type_iff:
  assumes t: "wftrm t"
    and f: "arity f > 0"
  shows "f  funs_term (Γ t)  (f  funs_term t  (x  fv t. f  funs_term (Γ (Var x))))"
    (is "?P t  ?Q t")
using t
proof (induction t)
  case (Fun g T)
  hence IH: "?P s  ?Q s" when "s  set T" for s
    using that wf_trm_subterm[OF _ Fun_param_is_subterm]
    by blast
  have 0: "arity g = length T" using Fun.prems unfolding wftrm_def by auto
  show ?case
  proof (cases "f = g")
    case True thus ?thesis using fun_type[OF f] by simp
  next
    case False
    have "?P (Fun g T)  (s  set T. ?P s)"
    proof
      assume *: "?P (Fun g T)"
      hence "Γ (Fun g T) = TComp g (map Γ T)"
        using const_type[of g] fun_type[of g] by force
      thus "s  set T. ?P s" using False * by force
    next
      assume *: "s  set T. ?P s"
      hence "Γ (Fun g T) = TComp g (map Γ T)"
        using 0 const_type[of g] fun_type[of g] by force
      thus "?P (Fun g T)" using False * by force
    qed
    thus ?thesis using False f IH by auto
  qed
qed simp

lemma funs_term_type_iff':
  assumes M: "wftrms M"
    and f: "arity f > 0"
  shows "f  (funs_term ` Γ ` M) 
        (f  (funs_term ` M)  (x  fvset M. f  funs_term (Γ (Var x))))" (is "?A  ?B")
proof
  assume ?A
  then obtain t where "t  M" "wftrm t" "f  funs_term (Γ t)" using M by atomize_elim auto
  thus ?B using funs_term_type_iff[OF _ f, of t] by auto
next
  assume ?B
  then obtain t where "t  M" "wftrm t" "f  funs_term t  (x  fv t. f  funs_term (Γ (Var x)))"
    using M by auto
  thus ?A using funs_term_type_iff[OF _ f, of t] by blast
qed

lemma Ana_subterm_type:
  assumes "Ana t = (K,M)"
    and "wftrm t"
    and "m  set M"
  shows "Γ m  Γ t"
proof -
  have "m  t" using Ana_subterm[OF assms(1)] assms(3) by auto
  thus ?thesis using subtermeq_imp_subtermtypeeq[OF assms(2)] by simp
qed

lemma wf_trm_TAtom_subterms:
  assumes "wftrm t" "Γ t = TAtom τ"
  shows "subterms t = {t}"
using assms const_type_inv unfolding wftrm_def by (cases t) force+

lemma wf_trm_TComp_subterm:
  assumes "wftrm s" "t  s"
  obtains f T where "Γ s = TComp f T"
proof (cases s)
  case (Var x) thus ?thesis using t  s by simp
next
  case (Fun g S)
  hence "length S > 0" using assms Fun_subterm_inside_params[of t g S] by auto
  hence "arity g > 0" by (metis wftrm s s = Fun g S term.order_refl wftrm_def) 
  thus ?thesis using fun_type s = Fun g S that by auto
qed

lemma SMP_empty[simp]: "SMP {} = {}"
proof (rule ccontr)
  assume "SMP {}  {}"
  then obtain t where "t  SMP {}" by auto
  thus False by (induct t rule: SMP.induct) auto
qed

lemma SMP_I:
  assumes "s  M" "wtsubst δ" "t  s  δ" "v. wftrm (δ v)"
  shows "t  SMP M"
using SMP.Substitution[OF SMP.MP[OF assms(1)] assms(2)] SMP.Subterm[of "s  δ" M t] assms(3,4)
by (cases "t = s  δ") simp_all

lemma SMP_wf_trm:
  assumes "t  SMP M" "wftrms M"
  shows "wftrm t"
using assms(1)
by (induct t rule: SMP.induct)
   (use assms(2) in blast,
    use wf_trm_subtermeq in blast,
    use wf_trm_subst in blast,
    use Ana_keys_wf' in blast)

lemma SMP_ikI[intro]: "t  ikst S  t  SMP (trmsst S)" by force

lemma MP_setI[intro]: "x  set S  trmsstp x  trmsst S" by force

lemma SMP_setI[intro]: "x  set S  trmsstp x  SMP (trmsst S)" by force

lemma SMP_subset_I:
  assumes M: "t  M. s δ. s  N  wtsubst δ  wftrms (subst_range δ)  t = s  δ"
  shows "SMP M  SMP N"
proof
  fix t show "t  SMP M  t  SMP N"
  proof (induction t rule: SMP.induct)
    case (MP t)
    then obtain s δ where s: "s  N" "wtsubst δ" "wftrms (subst_range δ)" "t = s  δ"
      using M by atomize_elim auto
    show ?case using SMP_I[OF s(1,2), of "s  δ"] s(3,4) wf_trm_subst_range_iff by fast
  qed (auto intro!: SMP.Substitution[of _ N])
qed

lemma SMP_union: "SMP (A  B) = SMP A  SMP B"
proof
  show "SMP (A  B)  SMP A  SMP B"
  proof
    fix t assume "t  SMP (A  B)"
    thus "t  SMP A  SMP B" by (induct rule: SMP.induct) blast+
  qed

  { fix t assume "t  SMP A" hence "t  SMP (A  B)" by (induct rule: SMP.induct) blast+ }
  moreover { fix t assume "t  SMP B" hence "t  SMP (A  B)" by (induct rule: SMP.induct) blast+ }
  ultimately show "SMP A  SMP B  SMP (A  B)" by blast
qed

lemma SMP_append[simp]: "SMP (trmsst (S@S')) = SMP (trmsst S)  SMP (trmsst S')" (is "?A = ?B")
using SMP_union by simp

lemma SMP_mono: "A  B  SMP A  SMP B"
proof -
  assume "A  B"
  then obtain C where "B = A  C" by atomize_elim auto
  thus "SMP A  SMP B" by (simp add: SMP_union)
qed

lemma SMP_Union: "SMP (m  M. f m) = (m  M. SMP (f m))"
proof
  show "SMP (mM. f m)  (mM. SMP (f m))"
  proof
    fix t assume "t  SMP (mM. f m)"
    thus "t  (mM. SMP (f m))" by (induct t rule: SMP.induct) force+
  qed
  show "(mM. SMP (f m))  SMP (mM. f m)"
  proof
    fix t assume "t  (mM. SMP (f m))"
    then obtain m where "m  M" "t  SMP (f m)" by atomize_elim auto
    thus "t  SMP (mM. f m)" using SMP_mono[of "f m" "mM. f m"] by auto
  qed
qed

lemma SMP_singleton_ex:
  "t  SMP M  (m  M. t  SMP {m})"
  "m  M  t  SMP {m}  t  SMP M"
using SMP_Union[of "λt. {t}" M] by auto

lemma SMP_Cons: "SMP (trmsst (x#S)) = SMP (trmsst [x])  SMP (trmsst S)"
using SMP_append[of "[x]" S] by auto

lemma SMP_Nil[simp]: "SMP (trmsst []) = {}" 
proof -
  { fix t assume "t  SMP (trmsst [])" hence False by induct auto }
  thus ?thesis by blast
qed

lemma SMP_subset_union_eq: assumes "M  SMP N" shows "SMP N = SMP (M  N)"
proof -
  { fix t assume "t  SMP (M  N)" hence "t  SMP N"
      using assms by (induction rule: SMP.induct) blast+
  }
  thus ?thesis using SMP_union by auto
qed

lemma SMP_subterms_subset: "subtermsset M  SMP M"
proof
  fix t assume "t  subtermsset M"
  then obtain m where "m  M" "t  m" by auto
  thus "t  SMP M" using SMP_I[of _ _ Var] by auto
qed

lemma SMP_SMP_subset: "N  SMP M  SMP N  SMP M"
by (metis SMP_mono SMP_subset_union_eq Un_commute Un_upper2)

lemma wt_subst_rm_vars: "wtsubst δ  wtsubst (rm_vars X δ)"
using rm_vars_dom unfolding wtsubst_def by auto

lemma wt_subst_SMP_subset:
  assumes "trmsst S  SMP S'" "wtsubst δ" "wftrms (subst_range δ)"
  shows "trmsst (S st δ)  SMP S'"
proof
  fix t assume *: "t  trmsst (S st δ)"
  show "t  SMP S'" using trm_strand_subst_cong(2)[OF *]
  proof
    assume "t'. t = t'  δ  t'  trmsst S"
    thus "t  SMP S'" using assms SMP.Substitution by auto
  next
    assume "X F. Inequality X F  set S  (t'trmspairs F. t = t'  rm_vars (set X) δ)"
    then obtain X F t' where **:
        "Inequality X F  set S" "t'trmspairs F" "t = t'  rm_vars (set X) δ"
      by force
    then obtain s where s: "s  trmsstp (Inequality X F)" "t = s  rm_vars (set X) δ" by atomize_elim auto
    hence "s  SMP (trmsst S)" using **(1) by force
    hence "t  SMP (trmsst S)"
      using SMP.Substitution[OF _ wt_subst_rm_vars[OF assms(2)] wf_trms_subst_rm_vars'[OF assms(3)]]
      unfolding s(2) by blast
    thus "t  SMP S'" by (metis SMP_union SMP_subset_union_eq UnCI assms(1))
  qed
qed

lemma MP_subset_SMP: "(trmsstp ` set S)  SMP (trmsst S)" "trmsst S  SMP (trmsst S)" "M  SMP M"
by auto

lemma SMP_fun_map_snd_subset: "SMP (trmsst (map Send1 X))  SMP (trmsst [Send1 (Fun f X)])"
proof
  fix t assume "t  SMP (trmsst (map Send1 X))" thus "t  SMP (trmsst [Send1 (Fun f X)])"
  proof (induction t rule: SMP.induct)
    case (MP t)
    hence "t  set X" by auto
    hence "t  Fun f X" by (metis subtermI')
    thus ?case using SMP.Subterm[of "Fun f X" "trmsst [Send1 (Fun f X)]" t] using SMP.MP by auto
  qed blast+
qed

lemma SMP_wt_subst_subset:
  assumes "t  SMP (M set )" "wtsubst " "wftrms (subst_range )"
  shows "t  SMP M"
using assms wf_trm_subst_range_iff[of ] by (induct t rule: SMP.induct) blast+

lemma SMP_wt_instances_subset:
  assumes "t  M. s  N. δ. t = s  δ  wtsubst δ  wftrms (subst_range δ)"
    and "t  SMP M"
  shows "t  SMP N"
proof -
  obtain m where m: "m  M" "t  SMP {m}" using SMP_singleton_ex(1)[OF assms(2)] by blast
  then obtain n δ where n: "n  N" "m = n  δ" "wtsubst δ" "wftrms (subst_range δ)"
    using assms(1) by fast

  have "t  SMP (N set δ)" using n(1,2) SMP_singleton_ex(2)[of m "N set δ", OF _ m(2)] by fast
  thus ?thesis using SMP_wt_subst_subset[OF _ n(3,4)] by blast
qed

lemma SMP_consts:
  assumes "t  M. c. t = Fun c []"
    and "t  M. Ana t = ([], [])"
  shows "SMP M = M"
proof
  show "SMP M  M"
  proof
    fix t show "t  SMP M  t  M"
      apply (induction t rule: SMP.induct)
      by (use assms in auto)
  qed
qed auto

lemma SMP_subterms_eq:
  "SMP (subtermsset M) = SMP M"
proof
  show "SMP M  SMP (subtermsset M)" using SMP_mono[of M "subtermsset M"] by blast
  show "SMP (subtermsset M)  SMP M"
  proof
    fix t show "t  SMP (subtermsset M)  t  SMP M" by (induction t rule: SMP.induct) blast+
  qed
qed

lemma SMP_funs_term:
  assumes t: "t  SMP M" "f  funs_term t  (x  fv t. f  funs_term (Γ (Var x)))"
    and f: "arity f > 0"
    and M: "wftrms M"
    and Ana_f: "s K T. Ana s = (K,T)  f  (funs_term ` set K)  f  funs_term s"
  shows "f  (funs_term ` M)  (x  fvset M. f  funs_term (Γ (Var x)))"
using t
proof (induction t rule: SMP.induct)
  case (Subterm t t')
  thus ?case by (metis UN_I vars_iff_subtermeq funs_term_subterms_eq(1) term.order_trans)
next
  case (Substitution t δ)
  show ?case
    using M SMP_wf_trm[OF Substitution.hyps(1)] wf_trm_subst[of δ t, OF Substitution.hyps(3)]
          funs_term_type_iff[OF _ f] wt_subst_trm''[OF Substitution.hyps(2), of t]
          Substitution.prems Substitution.IH
    by metis
next
  case (Ana t K T t')
  thus ?case
    using Ana_f[OF Ana.hyps(2)] Ana_keys_fv[OF Ana.hyps(2)]
    by fastforce
qed auto

lemma id_type_eq:
  assumes "Γ (Fun f X) = Γ (Fun g Y)"
  shows "f  𝒞  g  𝒞" "f  Σf  g  Σf"
using assms const_type' fun_type' id_union_univ(1)
by (metis UNIV_I UnE "term.distinct"(1))+

lemma fun_type_arg_cong:
  assumes "f  Σf" "g  Σf" "Γ (Fun f (x#X)) = Γ (Fun g (y#Y))"
  shows "Γ x = Γ y" "Γ (Fun f X) = Γ (Fun g Y)"
using assms fun_type' by auto

lemma fun_type_arg_cong':
  assumes "f  Σf" "g  Σf" "Γ (Fun f (X@x#X')) = Γ (Fun g (Y@y#Y'))" "length X = length Y"
  shows "Γ x = Γ y"
using assms
proof (induction X arbitrary: Y)
  case Nil thus ?case using fun_type_arg_cong(1)[of f g x X' y Y'] by auto
next
  case (Cons x' X Y'')
  then obtain y' Y where "Y'' = y'#Y" by (metis length_Suc_conv)
  hence "Γ (Fun f (X@x#X')) = Γ (Fun g (Y@y#Y'))" "length X = length Y"
    using Cons.prems(3,4) fun_type_arg_cong(2)[OF Cons.prems(1,2), of x' "X@x#X'"] by auto
  thus ?thesis using Cons.IH[OF Cons.prems(1,2)] by auto
qed

lemma fun_type_param_idx: "Γ (Fun f T) = Fun g S  i < length T  Γ (T ! i) = S ! i"
by (metis fun_type fun_type_id_eq fun_type_inv(1) nth_map term.inject(2))

lemma fun_type_param_ex:
  assumes "Γ (Fun f T) = Fun g (map Γ S)" "t  set S"
  shows "s  set T. Γ s = Γ t"
using fun_type_length_eq[OF assms(1)] length_map[of Γ S] assms(2)
      fun_type_param_idx[OF assms(1)] nth_map in_set_conv_nth
by metis

lemma tfr_stp_all_split:
  "list_all tfrstp (x#S)  list_all tfrstp [x]"
  "list_all tfrstp (x#S)  list_all tfrstp S"
  "list_all tfrstp (S@S')  list_all tfrstp S"
  "list_all tfrstp (S@S')  list_all tfrstp S'"
  "list_all tfrstp (S@x#S')  list_all tfrstp (S@S')"
by fastforce+

lemma tfr_stp_all_append:
  assumes "list_all tfrstp S" "list_all tfrstp S'"
  shows "list_all tfrstp (S@S')"
using assms by fastforce

lemma tfr_stp_all_wt_subst_apply:
  assumes "list_all tfrstp S"
    and θ: "wtsubst θ" "wftrms (subst_range θ)"
           "bvarsst S  range_vars θ = {}"
  shows "list_all tfrstp (S st θ)"
using assms(1,4)
proof (induction S)
  case (Cons x S)
  hence IH: "list_all tfrstp (S st θ)"
    using tfr_stp_all_split(2)[of x S]
    unfolding range_vars_alt_def by fastforce
  thus ?case
  proof (cases x)
    case (Equality a t t')
    hence "(δ. Unifier δ t t')  Γ t = Γ t'" using Cons.prems by auto
    hence "(δ. Unifier δ (t  θ) (t'  θ))  Γ (t  θ) = Γ (t'  θ)"
      by (metis Unifier_comp' wt_subst_trm'[OF assms(2)])
    moreover have "(x#S) st θ = Equality a (t  θ) (t'  θ)#(S st θ)"
      using x = Equality a t t' by auto
    ultimately show ?thesis using IH by auto
  next
    case (Inequality X F)
    let  = "rm_vars (set X) θ"
    let ?G = "F pairs "

    let ?P = "λF X. x  fvpairs F - set X. a. Γ (Var x) = TAtom a"
    let ?Q = "λF X.
      f T. Fun f T  subtermsset (trmspairs F)  T = []  (s  set T. s  Var ` set X)"

    have 0: "set X  range_vars  = {}"
      using Cons.prems(2) Inequality rm_vars_img_subset[of "set X"]
      by (auto simp add: subst_domain_def range_vars_alt_def)

    have 1: "?P F X  ?Q F X" using Inequality Cons.prems by simp

    have 2: "fvset ( ` set X) = set X" by auto

    have "?P ?G X" when "?P F X" using that
    proof (induction F)
      case (Cons g G)
      obtain t t' where g: "g = (t,t')" by (metis surj_pair)
      
      have "x  (fv (t  )  fv (t'  )) - set X. a. Γ (Var x) = Var a"
      proof -
        have *: "x  fv t - set X. a. Γ (Var x) = Var a"
               "x  fv t' - set X. a. Γ (Var x) = Var a"
          using g Cons.prems by simp_all

        have **: "x. wftrm ( x)"
          using θ(2) wf_trm_subst_range_iff[of θ] wf_trm_subst_rm_vars'[of θ _ "set X"] by simp

        show ?thesis
          using wt_subst_TAtom_fv[OF wt_subst_rm_vars[OF θ(1)] ** *(1)]
                wt_subst_TAtom_fv[OF wt_subst_rm_vars[OF θ(1)] ** *(2)]
                wt_subst_trm'[OF wt_subst_rm_vars[OF θ(1), of "set X"]] 2
          by blast
      qed
      moreover have "xfvpairs (G pairs ) - set X. a. Γ (Var x) = Var a"
        using Cons by auto
      ultimately show ?case using g by (auto simp add: subst_apply_pairs_def)
    qed (simp add: subst_apply_pairs_def)
    hence "?P ?G X  ?Q ?G X"
      using 1 ineq_subterm_inj_cond_subst[OF 0, of "trmspairs F"] trmspairs_subst[of F ]
      by presburger
    moreover have "(x#S) st θ = Inequality X (F pairs )#(S st θ)"
      using x = Inequality X F by auto
    ultimately show ?thesis using IH by simp
  qed auto
qed simp

lemma tfr_stp_all_same_type:
  "list_all tfrstp (S@Equality a t t'#S')  Unifier δ t t'  Γ t = Γ t'"
by force+

lemma tfr_subset:
  "A B. tfrset (A  B)  tfrset A"
  "A B. tfrset B  A  B  tfrset A"
  "A B. tfrset B  SMP A  SMP B  tfrset A"
proof -
  show 1: "tfrset (A  B)  tfrset A" for A B
    using SMP_union[of A B] unfolding tfrset_def by simp

  fix A B assume B: "tfrset B"

  show "A  B  tfrset A"
  proof -
    assume "A  B"
    then obtain C where "B = A  C" by atomize_elim auto
    thus ?thesis using B 1 by blast
  qed

  show "SMP A  SMP B  tfrset A"
  proof -
    assume "SMP A  SMP B"
    then obtain C where "SMP B = SMP A  C" by atomize_elim auto
    thus ?thesis using B unfolding tfrset_def by blast
  qed
qed

lemma tfr_empty[simp]: "tfrset {}"
unfolding tfrset_def by simp

lemma tfr_consts_mono:
  assumes "t  M. c. t = Fun c []"
    and "t  M. Ana t = ([], [])"
    and "tfrset N"
  shows "tfrset (N  M)"
proof -
  { fix s t
    assume *: "s  SMP (N  M) - range Var" "t  SMP (N  M) - range Var" "δ. Unifier δ s t"
    hence **: "is_Fun s" "is_Fun t" "s  SMP N  s  M" "t  SMP N  t  M"
      using assms(3) SMP_consts[OF assms(1,2)] SMP_union[of N M] by auto
    moreover have "Γ s = Γ t" when "s  SMP N" "t  SMP N"
      using that assms(3) *(3) **(1,2) unfolding tfrset_def by blast
    moreover have "Γ s = Γ t" when st: "s  M" "t  M"
    proof -
      obtain c d where "s = Fun c []" "t = Fun d []" using st assms(1) by atomize_elim auto
      hence "s = t" using *(3) by fast
      thus ?thesis by metis
    qed
    moreover have "Γ s = Γ t" when st: "s  SMP N" "t  M"
    proof -
      obtain c where "t = Fun c []" using st assms(1) by atomize_elim auto
      hence "s = t" using *(3) **(1,2) by auto
      thus ?thesis by metis
    qed
    moreover have "Γ s = Γ t" when st: "s  M" "t  SMP N"
    proof -
      obtain c where "s = Fun c []" using st assms(1) by atomize_elim auto
      hence "s = t" using *(3) **(1,2) by auto
      thus ?thesis by metis
    qed
    ultimately have "Γ s = Γ t" by metis
  } thus ?thesis by (metis tfrset_def)
qed

lemma dualst_tfrstp: "list_all tfrstp S  list_all tfrstp (dualst S)"
proof (induction S)
  case (Cons x S)
  have "list_all tfrstp S" using Cons.prems by simp
  hence IH: "list_all tfrstp (dualst S)" using Cons.IH by metis
  from Cons show ?case
  proof (cases x)
    case (Equality a t t')
    hence "(δ. Unifier δ t t')  Γ t = Γ t'" using Cons by auto
    thus ?thesis using Equality IH by fastforce
  next
    case (Inequality X F)
    have "set (dualst (x#S)) = insert x (set (dualst S))" using Inequality by auto
    moreover have "(x  fvpairs F - set X. a. Γ (Var x) = Var a) 
            (f T. Fun f T  subtermsset (trmspairs F)  T = []  (s  set T. s  Var ` set X))" 
      using Cons.prems Inequality by auto
    ultimately show ?thesis using Inequality IH by auto
  qed auto
qed simp

lemma subst_var_inv_wt:
  assumes "wtsubst δ"
  shows "wtsubst (subst_var_inv δ X)"
using assms f_inv_into_f[of _ δ X]
unfolding wtsubst_def subst_var_inv_def
by presburger

lemma subst_var_inv_wf_trms:
  "wftrms (subst_range (subst_var_inv δ X))"
using f_inv_into_f[of _ δ X]
unfolding wtsubst_def subst_var_inv_def
by auto

lemma unify_list_wt_if_same_type:
  assumes "Unification.unify E B = Some U" "(s,t)  set E. wftrm s  wftrm t  Γ s = Γ t"
  and "(v,t)  set B. Γ (Var v) = Γ t"
  shows "(v,t)  set U. Γ (Var v) = Γ t"
using assms
proof (induction E B arbitrary: U rule: Unification.unify.induct)
  case (2 f X g Y E B U)
  hence "wftrm (Fun f X)" "wftrm (Fun g Y)" "Γ (Fun f X) = Γ (Fun g Y)" by auto

  from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'"
    and [simp]: "f = g" "length X = length Y" "E' = zip X Y"
    and **: "Unification.unify (E'@E) B = Some U"
    by (auto split: option.splits)
  
  have "(s,t)  set E'. wftrm s  wftrm t  Γ s = Γ t"
  proof -
    { fix s t assume "(s,t)  set E'"
      then obtain X' X'' Y' Y'' where "X = X'@s#X''" "Y = Y'@t#Y''" "length X' = length Y'"
        using zip_arg_subterm_split[of s t X Y] E' = zip X Y by metis
      hence "Γ (Fun f (X'@s#X'')) = Γ (Fun g (Y'@t#Y''))" by (metis Γ (Fun f X) = Γ (Fun g Y))
      
      from E' = zip X Y have "(s,t)  set E'. s  Fun f X  t  Fun g Y"
        using zip_arg_subterm[of _ _ X Y] by blast
      with (s,t)  set E' have "wftrm s" "wftrm t"
        using wf_trm_subterm wftrm (Fun f X) wftrm (Fun g Y) by (blast,blast)
      moreover have "f  Σf"
      proof (rule ccontr)
        assume "f  Σf"
        hence "f  𝒞" "arity f = 0" using const_arity_eq_zero[of f] by simp_all
        thus False using wftrm (Fun f X) * (s,t)  set E' unfolding wftrm_def by auto
      qed
      hence "Γ s = Γ t"
        using fun_type_arg_cong' f  Σf Γ (Fun f (X'@s#X'')) = Γ (Fun g (Y'@t#Y''))
              length X' = length Y' f = g
        by metis
      ultimately have "wftrm s" "wftrm t" "Γ s = Γ t" by metis+
    }
    thus ?thesis by blast
  qed
  moreover have "(s,t)  set E. wftrm s  wftrm t  Γ s = Γ t" using "2.prems"(2) by auto
  ultimately show ?case using "2.IH"[OF * ** _ "2.prems"(3)] by fastforce
next
  case (3 v t E B U)
  hence "Γ (Var v) = Γ t" "wftrm t" by auto
  hence "wtsubst (subst v t)"
      and *: "(v, t)  set ((v,t)#B). Γ (Var v) = Γ t"
             "t t'. (t,t')  set E  Γ t = Γ t'"
    using "3.prems"(2,3) unfolding wtsubst_def subst_def by auto

  show ?case
  proof (cases "t = Var v")
    assume "t = Var v" thus ?case using 3 by auto
  next
    assume "t  Var v"
    hence "v  fv t" using "3.prems"(1) by auto
    hence **: "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using Unification.unify.simps(3)[of v t E B] "3.prems"(1) t  Var v by auto
    
    have "(s, t)  set (subst_list (subst v t) E). wftrm s  wftrm t"
      using wf_trm_subst_singleton[OF _ wftrm t] "3.prems"(2)
      unfolding subst_list_def subst_def by auto
    moreover have "(s, t)  set (subst_list (subst v t) E). Γ s = Γ t"
      using *(2)[THEN wt_subst_trm'[OF wtsubst (subst v t)]] by (simp add: subst_list_def)
    ultimately show ?thesis using "3.IH"(2)[OF t  Var v v  fv t ** _ *(1)] by auto
  qed
next
  case (4 f X v E B U)
  hence "Γ (Var v) = Γ (Fun f X)" "wftrm (Fun f X)" by auto
  hence "wtsubst (subst v (Fun f X))"
      and *: "(v, t)  set ((v,(Fun f X))#B). Γ (Var v) = Γ t"
             "t t'. (t,t')  set E  Γ t = Γ t'"
    using "4.prems"(2,3) unfolding wtsubst_def subst_def by auto

  have "v  fv (Fun f X)" using "4.prems"(1) by force
  hence **: "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, (Fun f X))#B) = Some U"
    using Unification.unify.simps(3)[of v "Fun f X" E B] "4.prems"(1) by auto
  
  have "(s, t)  set (subst_list (subst v (Fun f X)) E). wftrm s  wftrm t"
    using wf_trm_subst_singleton[OF _ wftrm (Fun f X)] "4.prems"(2)
    unfolding subst_list_def subst_def by auto
  moreover have "(s, t)  set (subst_list (subst v (Fun f X)) E). Γ s = Γ t"
    using *(2)[THEN wt_subst_trm'[OF wtsubst (subst v (Fun f X))]] by (simp add: subst_list_def)
  ultimately show ?case using "4.IH"[OF v  fv (Fun f X) ** _ *(1)] by auto
qed auto

lemma mgu_wt_if_same_type:
  assumes "mgu s t = Some σ" "wftrm s" "wftrm t" "Γ s = Γ t"
  shows "wtsubst σ"
proof -
  let ?fv_disj = "λv t S. ¬((v',t')  S - {(v,t)}. (insert v (fv t))  (insert v' (fv t'))  {})"

  from assms(1) obtain σ' where "Unification.unify [(s,t)] [] = Some σ'" "subst_of σ' = σ"
    by (auto simp: mgu_def split: option.splits)
  hence "(v,t)  set σ'. Γ (Var v) = Γ t" "distinct (map fst σ')"
    using assms(2,3,4) unify_list_wt_if_same_type unify_list_distinct[of "[(s,t)]"] by auto
  thus "wtsubst σ" using subst_of σ' = σ unfolding wtsubst_def
  proof (induction σ' arbitrary: σ rule: List.rev_induct)
    case (snoc tt σ' σ)
    then obtain v t where tt: "tt = (v,t)" by (metis surj_pair)
    hence σ: "σ = subst v t s subst_of σ'" using snoc.prems(3) by simp
    
    have "(v,t)  set σ'. Γ (Var v) = Γ t" "distinct (map fst σ')" using snoc.prems(1,2) by auto
    then obtain σ'' where σ'': "subst_of σ' = σ''" "v. Γ (Var v) = Γ (σ'' v)" by (metis snoc.IH)
    hence "Γ t = Γ (t  σ'')" for t using wt_subst_trm by blast
    hence "Γ (Var v) = Γ (σ'' v)" "Γ t = Γ (t  σ'')" using σ''(2) by auto
    moreover have "Γ (Var v) = Γ t" using snoc.prems(1) tt by simp
    moreover have σ2: "σ = Var(v := t) s σ'' " using σ σ''(1) unfolding subst_def by simp
    ultimately have "Γ (Var v) = Γ (σ v)" unfolding subst_compose_def by simp

    have "subst_domain (subst v t)  {v}" unfolding subst_def by (auto simp add: subst_domain_def)
    hence *: "subst_domain σ  insert v (subst_domain σ'')"
      using tt σ σ''(1) snoc.prems(2) subst_domain_compose[of _ σ'']
      by (auto simp add: subst_domain_def)
    
    have "v  set (map fst σ')" using tt snoc.prems(2) by auto
    hence "v  subst_domain σ''" using σ''(1) subst_of_dom_subset[of σ'] by auto

    { fix w assume "w  subst_domain σ''"
      hence "σ w = σ'' w" using σ2 σ''(1) v  subst_domain σ'' unfolding subst_compose_def by auto
      hence "Γ (Var w) = Γ (σ w)" using σ''(2) by simp
    }
    thus ?case using Γ (Var v) = Γ (σ v) * by force
  qed simp
qed

lemma wt_Unifier_if_Unifier:
  assumes s_t: "wftrm s" "wftrm t" "Γ s = Γ t"
    and δ: "Unifier δ s t"
  shows "θ. Unifier θ s t  wtsubst θ  wftrms (subst_range θ)"
using mgu_always_unifies[OF δ] mgu_gives_MGU[THEN MGU_is_Unifier[of s _ t]]
      mgu_wt_if_same_type[OF _ s_t] mgu_wf_trm[OF _ s_t(1,2)] wf_trm_subst_range_iff
by fast

end


subsection ‹Automatically Proving Type-Flaw Resistance›
subsubsection ‹Definitions: Variable Renaming›
abbreviation "max_var t  Max (insert 0 (snd ` fv t))"
abbreviation "max_var_set X  Max (insert 0 (snd ` X))"

definition "var_rename n v  Var (fst v, snd v + Suc n)"
definition "var_rename_inv n v  Var (fst v, snd v - Suc n)"


subsubsection ‹Definitions: Computing a Finite Representation of the Sub-Message Patterns›
text ‹A sufficient requirement for a term to be a well-typed instance of another term›
definition is_wt_instance_of_cond where
  "is_wt_instance_of_cond Γ t s  (
    Γ t = Γ s  (case mgu t s of
      None  False
    | Some δ  inj_on δ (fv t)  (x  fv t. is_Var (δ x))))"

definition has_all_wt_instances_of where
  "has_all_wt_instances_of Γ N M  t  N. s  M. is_wt_instance_of_cond Γ t s"

text ‹This function computes a finite representation of the set of sub-message patterns›
definition SMP0 where
  "SMP0 Ana Γ M  let
      f = λt. Fun (the_Fun (Γ t)) (map Var (zip (args (Γ t)) [0..<length (args (Γ t))]));
      g = λM'. map f (filter (λt. is_Var t  is_Fun (Γ t)) M')@
               concat (map (fst  Ana) M')@concat (map subterms_list M');
      h = remdups  g
    in while (λA. set (h A)  set A) h M"

text ‹These definitions are useful to refine an SMP representation set›
fun generalize_term where
  "generalize_term _ _ n (Var x) = (Var x, n)"
| "generalize_term Γ p n (Fun f T) = (let τ = Γ (Fun f T)
    in if p τ then (Var (τ, n), Suc n)
       else let (T',n') = foldr (λt (S,m). let (t',m') = generalize_term Γ p m t in (t'#S,m'))
                                T ([],n)
            in (Fun f T', n'))"

definition generalize_terms where
  "generalize_terms Γ p  map (fst  generalize_term Γ p 0)"

definition remove_superfluous_terms where
  "remove_superfluous_terms Γ T 
    let
      f = λS t R. s  set S - R. s  t  is_wt_instance_of_cond Γ t s;
      g = λS t (U,R). if f S t R then (U, insert t R) else (t#U, R);
      h = λS. remdups (fst (foldr (g S) S ([],{})))
    in while (λS. h S  S) h T"


subsubsection ‹Definitions: Checking Type-Flaw Resistance›
definition is_TComp_var_instance_closed where
  "is_TComp_var_instance_closed Γ M  x  fvset M. is_Fun (Γ (Var x)) 
      (t  M. is_Fun t  Γ t = Γ (Var x)  list_all is_Var (args t)  distinct (args t))"

definition finite_SMP_representation where
  "finite_SMP_representation arity Ana Γ M 
    (M = {}  card M > 0) 
    wftrms' arity M 
    has_all_wt_instances_of Γ (subtermsset M) M 
    has_all_wt_instances_of Γ (((set  fst  Ana) ` M)) M 
    is_TComp_var_instance_closed Γ M"

definition comp_tfrset where
  "comp_tfrset arity Ana Γ M 
    finite_SMP_representation arity Ana Γ M 
    (let δ = var_rename (max_var_set (fvset M))
     in s  M. t  M. is_Fun s  is_Fun t  Γ s  Γ t  mgu s (t  δ) = None)"

fun comp_tfrstp where
  "comp_tfrstp Γ (_: t  t'st) = (mgu t t'  None  Γ t = Γ t')"
| "comp_tfrstp Γ (X⟨∨≠: Fst) = (
    (x  fvpairs F - set X. is_Var (Γ (Var x))) 
    (u  subtermsset (trmspairs F).
      is_Fun u  (args u = []  (s  set (args u). s  Var ` set X))))"
| "comp_tfrstp _ _ = True"

definition comp_tfrst where
  "comp_tfrst arity Ana Γ M S 
    list_all (comp_tfrstp Γ) S 
    list_all (wftrm' arity) (trms_listst S) 
    has_all_wt_instances_of Γ (trmsst S) M 
    comp_tfrset arity Ana Γ M"


subsubsection ‹Small Lemmata›
lemma max_var_set_mono:
  assumes "finite N"
    and "M  N"
  shows "max_var_set M  max_var_set N"
by (meson assms Max.subset_imp finite.insertI finite_imageI image_mono insert_mono insert_not_empty) 

lemma less_Suc_max_var_set:
  assumes z: "z  X"
    and X: "finite X"
  shows "snd z < Suc (max_var_set X)"
proof -
  have "snd z  snd ` X" using z by simp
  hence "snd z  Max (insert 0 (snd ` X))" using X by simp
  thus ?thesis using X by simp
qed

lemma (in typed_model) finite_SMP_representationD:
  assumes "finite_SMP_representation arity Ana Γ M"
  shows "wftrms M"
    and "has_all_wt_instances_of Γ (subtermsset M) M"
    and "has_all_wt_instances_of Γ (((set  fst  Ana) ` M)) M"
    and "is_TComp_var_instance_closed Γ M"
    and "finite M"
using assms wftrms_code[of M] unfolding finite_SMP_representation_def list_all_iff card_gt_0_iff
by blast+

lemma (in typed_model) is_wt_instance_of_condD:
  assumes t_instance_s: "is_wt_instance_of_cond Γ t s"
  obtains δ where
    "Γ t = Γ s" "mgu t s = Some δ"
    "inj_on δ (fv t)" "δ ` (fv t)  range Var"
using t_instance_s unfolding is_wt_instance_of_cond_def Let_def by (cases "mgu t s") fastforce+

lemma (in typed_model) is_wt_instance_of_condD':
  assumes t_wf_trm: "wftrm t"
    and s_wf_trm: "wftrm s"
    and t_instance_s: "is_wt_instance_of_cond Γ t s"
  shows "δ. wtsubst δ  wftrms (subst_range δ)  t = s  δ"
proof -
  obtain δ where s:
      "Γ t = Γ s" "mgu t s = Some δ"
      "inj_on δ (fv t)" "δ ` (fv t)  range Var"
    by (metis is_wt_instance_of_condD[OF t_instance_s])

  have 0: "wftrm t" "wftrm s" using s(1) t_wf_trm s_wf_trm by auto

  note 1 = mgu_wt_if_same_type[OF s(2) 0 s(1)]

  note 2 = conjunct1[OF mgu_gives_MGU[OF s(2)]]

  show ?thesis
    using s(1) inj_var_ran_unifiable_has_subst_match[OF 2 s(3,4)]
          wt_subst_compose[OF 1 subst_var_inv_wt[OF 1, of "fv t"]]
          wf_trms_subst_compose[OF mgu_wf_trms[OF s(2) 0] subst_var_inv_wf_trms[of δ "fv t"]]
    by auto
qed

lemma (in typed_model) is_wt_instance_of_condD'':
  assumes s_wf_trm: "wftrm s"
    and t_instance_s: "is_wt_instance_of_cond Γ t s"
    and t_var: "t = Var x"
  shows "y. s = Var y  Γ (Var y) = Γ (Var x)"
proof -
  obtain δ where δ: "wtsubst δ" and s: "Var x = s  δ"
    using is_wt_instance_of_condD'[OF _ s_wf_trm t_instance_s] t_var by auto
  obtain y where y: "s = Var y" using s by (cases s) auto
  show ?thesis using wt_subst_trm''[OF δ] s y by metis
qed

lemma (in typed_model) has_all_wt_instances_ofD:
  assumes N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "t  N"
  obtains s δ where
    "s  M" "Γ t = Γ s" "mgu t s = Some δ"
    "inj_on δ (fv t)" "δ ` (fv t)  range Var"
by (metis t_in_N N_instance_M is_wt_instance_of_condD has_all_wt_instances_of_def)

lemma (in typed_model) has_all_wt_instances_ofD':
  assumes N_wf_trms: "wftrms N"
    and M_wf_trms: "wftrms M"
    and N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "t  N"
  shows "δ. wtsubst δ  wftrms (subst_range δ)  t  M set δ"
using assms is_wt_instance_of_condD' unfolding has_all_wt_instances_of_def by fast

lemma (in typed_model) has_all_wt_instances_ofD'':
  assumes N_wf_trms: "wftrms N"
    and M_wf_trms: "wftrms M"
    and N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "Var x  N"
  shows "y. Var y  M  Γ (Var y) = Γ (Var x)"
using assms is_wt_instance_of_condD'' unfolding has_all_wt_instances_of_def by fast
  
lemma (in typed_model) has_all_instances_of_if_subset:
  assumes "N  M"
  shows "has_all_wt_instances_of Γ N M"
unfolding has_all_wt_instances_of_def
proof
  fix t assume t: "t  N"
  hence "is_wt_instance_of_cond Γ t t"
    using inj_onI[of "fv t"] mgu_same_empty[of t]
    unfolding is_wt_instance_of_cond_def by force
  thus "s  M. is_wt_instance_of_cond Γ t s" using t assms by blast
qed

lemma (in typed_model) SMP_I':
  assumes N_wf_trms: "wftrms N"
    and M_wf_trms: "wftrms M"
    and N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "t  N"
  shows "t  SMP M"
using has_all_wt_instances_ofD'[OF N_wf_trms M_wf_trms N_instance_M t_in_N]
      SMP.Substitution[OF SMP.MP[of _ M]]
by blast


subsubsection ‹Lemma: Proving Type-Flaw Resistance›
locale typed_model' = typed_model arity public Ana Γ
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,(('fun,'atom::finite) term_type × nat)) term
               (('fun,(('fun,'atom) term_type × nat)) term list
                 × ('fun,(('fun,'atom) term_type × nat)) term list)"
    and Γ::"('fun,(('fun,'atom) term_type × nat)) term  ('fun,'atom) term_type"
  +
  assumes Γ_Var_fst: "τ n m. Γ (Var (τ,n)) = Γ (Var (τ,m))"
    and Ana_const: "c T. arity c = 0  Ana (Fun c T) = ([],[])"
    and Ana_subst'_or_Ana_keys_subterm:
      "(f T δ K R. Ana (Fun f T) = (K,R)  Ana (Fun f T  δ) = (K list δ,R list δ)) 
       (t K R k. Ana t = (K,R)  k  set K  k  t)"
begin

lemma var_rename_inv_comp: "t  (var_rename n s var_rename_inv n) = t"
proof (induction t)
  case (Fun f T)
  hence "map (λt. t  var_rename n s var_rename_inv n) T = T" by (simp add: map_idI) 
  thus ?case by (metis eval_term.simps(2)) 
qed (simp add: var_rename_def var_rename_inv_def subst_compose)

lemma var_rename_fv_disjoint:
  "fv s  fv (t  var_rename (max_var s)) = {}"
proof -
  have 1: "v  fv s. snd v  max_var s" by simp
  have 2: "v  fv (t  var_rename n). snd v > n" for n unfolding var_rename_def by (induct t) auto
  show ?thesis using 1 2 by force
qed

lemma var_rename_fv_set_disjoint:
  assumes "finite M" "s  M"
  shows "fv s  fv (t  var_rename (max_var_set (fvset M))) = {}"
proof -
  have 1: "v  fv