(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2018

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  Title:      IntruderDeduction.thy
    Author:     Andreas Viktor Hess, DTU
*)

section {* Theory: Dolev-Yao Intruder Model *}
theory IntruderDeduction
imports Messages Unification2
begin

subsection {* Dolev-Yao intruder model locale *}
locale intruder_model =
  fixes arity :: "'fun::countable \<Rightarrow> nat"
    and public :: "'fun \<Rightarrow> bool"
    and Ana :: "('fun,'var::countable) term \<Rightarrow> (('fun,'var) terms \<times> ('fun,'var) terms)"
  assumes Ana_keys_FV: "\<And>t K T. Ana t = (K,T) \<Longrightarrow> FV\<^sub>s\<^sub>e\<^sub>t K \<subseteq> FV t"
    and Ana_keys_finite: "\<And>t K T. Ana t = (K,T) \<Longrightarrow> finite K"
    and Ana_keys_wf: "\<And>t k K T f S.
      Ana t = (K,T) \<Longrightarrow> (\<And>g S'. Fun g S' \<sqsubseteq> t \<Longrightarrow> length S' = arity g)
        \<Longrightarrow> k \<in> K \<Longrightarrow> Fun f S \<sqsubseteq> k \<Longrightarrow> length S = arity f"
    and Ana_var[simp]: "\<And>x. Ana (Var x) = ({},{})"
    and Ana_fun_subterm: "\<And>f X K T. Ana (Fun f X) = (K,T) \<Longrightarrow> T \<subseteq> set X"
    and Ana_subst: "\<And>t \<delta> K M. \<lbrakk>Ana t = (K,M); K \<noteq> {} \<or> M \<noteq> {}\<rbrakk> \<Longrightarrow> Ana (t \<cdot> \<delta>) = (K \<cdot>set \<delta>,M \<cdot>set \<delta>)"
    and infinite_vars[simp]: "infinite (UNIV::'var set)"
    and infinite_public_consts[simp]: "infinite {c. public c \<and> arity c = 0}"
    and no_private_funs[simp]: "\<And>f. arity f > 0 \<Longrightarrow> public f"
begin

lemma Ana_subterm: assumes "Ana t = (K,T)" shows "T \<subset> subterms t"
proof (cases t)
  case Var thus ?thesis using Ana_var assms by auto
next
  case Fun thus ?thesis using Ana_fun_subterm assms by force
qed

lemma Ana_finite: assumes "Ana t = (K,M)" shows "finite K" "finite M"
by (metis Ana_keys_finite[OF assms],
    metis Ana_subterm[OF assms] finite_Un subterms_finite sup.strict_order_iff)

lemma Ana_vars: assumes "Ana t = (K,M)" shows "FV\<^sub>s\<^sub>e\<^sub>t K \<subseteq> FV t" "FV\<^sub>s\<^sub>e\<^sub>t M \<subseteq> FV t"
apply (rule Ana_keys_FV[OF assms])
using Ana_subterm[OF assms] subtermeqI[THEN subtermeq_vars_subset]
by auto

definition \<V> where "\<V> \<equiv> UNIV::'var set"
definition \<Sigma>n ("\<Sigma>\<^sup>_") where "\<Sigma>\<^sup>n \<equiv> {f::'fun. arity f = n}"
definition \<Sigma>npub ("\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>_") where "\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n \<equiv> {f. public f} \<inter> \<Sigma>\<^sup>n"
definition \<Sigma>npriv ("\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>_") where "\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n \<equiv> {f. \<not>public f} \<inter> \<Sigma>\<^sup>n"
definition \<Sigma>\<^sub>p\<^sub>u\<^sub>b where "\<Sigma>\<^sub>p\<^sub>u\<^sub>b \<equiv> (\<Union>n. \<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n)"
definition \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> (\<Union>n. \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n)"
definition \<Sigma> where "\<Sigma> \<equiv> (\<Union>n. \<Sigma>\<^sup>n)"
definition \<C> where "\<C> \<equiv> \<Sigma>\<^sup>0"
definition \<C>\<^sub>p\<^sub>u\<^sub>b where "\<C>\<^sub>p\<^sub>u\<^sub>b \<equiv> {f. public f} \<inter> \<C>"
definition \<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> {f. \<not>public f} \<inter> \<C>"
definition \<Sigma>\<^sub>f where "\<Sigma>\<^sub>f \<equiv> \<Sigma> - \<C>"
definition \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b where "\<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<equiv> \<Sigma>\<^sub>f \<inter> \<Sigma>\<^sub>p\<^sub>u\<^sub>b"
definition \<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> \<Sigma>\<^sub>f \<inter> \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v"
declare \<V>_def[simp] \<Sigma>n_def[simp] \<Sigma>npub_def[simp] \<Sigma>npriv_def[simp] \<Sigma>\<^sub>p\<^sub>u\<^sub>b_def[simp] \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v_def[simp]
        \<Sigma>_def[simp] \<C>_def[simp] \<C>\<^sub>p\<^sub>u\<^sub>b_def[simp] \<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v_def[simp] \<Sigma>\<^sub>f_def[simp] \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b_def[simp]
        \<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v_def[simp]

lemma disjoint_fun_syms: "\<Sigma>\<^sub>f \<inter> \<C> = {}" by auto
lemma id_union_univ: "\<Sigma>\<^sub>f \<union> \<C> = UNIV" "\<Sigma> = UNIV" by auto
lemma const_arity_eq_zero[dest]: "c \<in> \<C> \<Longrightarrow> arity c = 0" by simp
lemma const_pub_arity_eq_zero[dest]: "c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> arity c = 0 \<and> public c" by simp
lemma const_priv_arity_eq_zero[dest]: "c \<in> \<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<Longrightarrow> arity c = 0 \<and> \<not>public c" by simp
lemma fun_arity_gt_zero[dest]: "f \<in> \<Sigma>\<^sub>f \<Longrightarrow> arity f > 0" by fastforce
lemma pub_fun_public[dest]: "f \<in> \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> public f" by fastforce
lemma pub_fun_arity_gt_zero[dest]: "f \<in> \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> arity f > 0" by fastforce

lemma countable_vars[simp]: "countable \<V>" by (rule countableI_type)

lemma countable_fun_syms[simp]: "countable \<Sigma>\<^sub>f" "countable \<C>" "countable (UNIV::'fun set)"
by (rule countableI_type)+

lemma \<Sigma>\<^sub>f_unfold: "\<Sigma>\<^sub>f = {f::'fun. arity f > 0}" by auto
lemma \<C>_unfold: "\<C> = {f::'fun. arity f = 0}" by auto
lemma \<C>pub_unfold: "\<C>\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f = 0 \<and> public f}" by auto
lemma \<C>priv_unfold: "\<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f = 0 \<and> \<not>public f}" by auto
lemma \<Sigma>npub_unfold: "\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n = {f::'fun. arity f = n \<and> public f}" by auto
lemma \<Sigma>npriv_unfold: "\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n = {f::'fun. arity f = n \<and> \<not>public f}" by auto
lemma \<Sigma>fpub_unfold: "\<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f > 0 \<and> public f}" by auto
lemma \<Sigma>fpriv_unfold: "\<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f > 0 \<and> \<not>public f}" by auto
lemma \<Sigma>n_m_eq: "\<lbrakk>(\<Sigma>\<^sup>n) \<noteq> {}; (\<Sigma>\<^sup>n) = (\<Sigma>\<^sup>m)\<rbrakk> \<Longrightarrow> n = m" by auto

lemma infinite_fun_syms[simp]:
  "infinite {c. public c \<and> arity c > 0} \<Longrightarrow> infinite \<Sigma>\<^sub>f" "infinite \<C>" "infinite \<C>\<^sub>p\<^sub>u\<^sub>b"
  "infinite (UNIV::'fun set)"
using finite_Collect_conjI infinite_public_consts apply (metis \<Sigma>\<^sub>f_unfold, metis \<Sigma>n_def \<C>_def)
using infinite_public_consts \<C>pub_unfold apply (simp add: Collect_conj_eq)
by (metis UNIV_I finite_subset subsetI infinite_public_consts(1))

lemma id_univ_proper_subset[simp]: "\<Sigma>\<^sub>f \<subset> UNIV" "(\<exists>f. arity f > 0) \<Longrightarrow> \<C> \<subset> UNIV"
using finite.emptyI inf_top.right_neutral top.not_eq_extremum
apply (metis disjoint_fun_syms infinite_fun_syms(2) inf_commute)
by (metis top.not_eq_extremum UNIV_I const_arity_eq_zero less_irrefl)


subsubsection {* Term well-formedness *}
definition wf\<^sub>t\<^sub>r\<^sub>m where "wf\<^sub>t\<^sub>r\<^sub>m t \<equiv> \<forall>f T. Fun f T \<sqsubseteq> t \<longrightarrow> length T = arity f"

lemma Ana_keys_wf': "Ana t = (K,T) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> k \<in> K \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m k"
using Ana_keys_wf unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by metis

lemma wf_trm_Var[simp]: "wf\<^sub>t\<^sub>r\<^sub>m (Var x)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by simp

lemma wf_trm_img_subst: "(\<forall>t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>. wf\<^sub>t\<^sub>r\<^sub>m t) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> v)"
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (cases "\<sigma> v \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>") auto

lemma wf_trmI[intro]:
  assumes "\<And>x. x \<in> set X \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m x" "length X = arity f"
  shows "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)"
using assms unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto

lemma wf_trm_subst:
  assumes "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)" "wf\<^sub>t\<^sub>r\<^sub>m t"
  shows "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)"
using \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>
proof (induction t)
  case (Fun f X)
  hence "\<And>x. x \<in> set X \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m x"
    by (meson wf\<^sub>t\<^sub>r\<^sub>m_def Fun_param_is_subterm subtermeq_trans subtermseq_if_subterms)
  hence "\<And>x. x \<in> set X \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (x \<cdot> \<delta>)" using Fun.IH by auto
  moreover have "length (map (\<lambda>x. x \<cdot> \<delta>) X) = arity f"
    using \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
  ultimately show ?case by fastforce
qed (simp add: \<open>\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)\<close>)

lemma wf_trm_subst_singleton:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" shows "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> Var(v := t'))"
proof -
  have "\<And>w. wf\<^sub>t\<^sub>r\<^sub>m ((Var(v := t')) w)" using \<open>wf\<^sub>t\<^sub>r\<^sub>m t'\<close> unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by simp
  thus ?thesis using wf_trm_subst[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>, of "Var(v := t')"] by simp
qed

lemma wf_trm_subterm: "\<lbrakk>wf\<^sub>t\<^sub>r\<^sub>m t; s \<sqsubset> t\<rbrakk> \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m s"
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (induct t) auto

lemma wf_trm_subtermeq:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t"
  shows "wf\<^sub>t\<^sub>r\<^sub>m s"
proof (cases "s = t")
  case False thus "wf\<^sub>t\<^sub>r\<^sub>m s" using assms(2) wf_trm_subterm[OF assms(1)] by simp
qed (metis assms(1))

lemma unify_list_wf_trm:
  assumes "Unification.unify E B = Some U" "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
  and "\<forall>(v,t) \<in> set B. wf\<^sub>t\<^sub>r\<^sub>m t"
  shows "\<forall>(v,t) \<in> set U. wf\<^sub>t\<^sub>r\<^sub>m t"
using assms
proof (induction E B arbitrary: U rule: Unification.unify.induct)
  case (1 B U) thus ?case by auto
next
  case (2 f X g Y E B U)
  have wf_fun: "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun g Y)" using "2.prems"(2) 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)
  hence "\<And>t t'. (t,t') \<in> set E' \<Longrightarrow> t \<sqsubset> Fun f X \<and> t' \<sqsubset> Fun g Y" by (metis zip_arg_subterm)
  hence "\<And>t t'. (t,t') \<in> set E' \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t \<and> wf\<^sub>t\<^sub>r\<^sub>m t'"
    using wf_trm_subterm wf_fun \<open>f = g\<close> by blast+
  thus ?case using "2.IH"[OF * ** _ "2.prems"(3)] "2.prems"(2) by fastforce
next
  case (3 v t E B)
  hence *: "\<forall>(w,x) \<in> set ((v, t) # B). wf\<^sub>t\<^sub>r\<^sub>m x"
      and **: "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t"
    by auto

  show ?case
  proof (cases "t = Var v")
    case True thus ?thesis using "3.prems" "3.IH"(1) by auto
  next
    case False
    hence "v \<notin> FV t" using "3.prems"(1) by auto
    hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using \<open>t \<noteq> Var v\<close> "3.prems"(1) by auto
    moreover have "\<forall>(s, t) \<in> set (subst_list (subst v t) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
      using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>] "3.prems"(2)
      unfolding subst_list_def subst_def by auto
    ultimately show ?thesis using "3.IH"(2)[OF \<open>t \<noteq> Var v\<close> \<open>v \<notin> FV t\<close> _ _ *] by metis
  qed
next
  case (4 f X v E B U)
  hence *: "\<forall>(w,x) \<in> set ((v, Fun f X) # B). wf\<^sub>t\<^sub>r\<^sub>m x"
      and **: "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)"
    by auto

  have "v \<notin> 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 "4.prems"(1) by auto
  moreover have "\<forall>(s, t) \<in> set (subst_list (subst v (Fun f X)) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
    using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close>] "4.prems"(2)
    unfolding subst_list_def subst_def by auto
  ultimately show ?case using "4.IH"[OF \<open>v \<notin> FV (Fun f X)\<close> _ _ *] by metis
qed

lemma mgu_wf_trm:
  assumes "mgu s t = Some \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t"
  shows "wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> v)"
proof -
  from assms obtain \<sigma>' where "subst_of \<sigma>' = \<sigma>" "\<forall>(v,t) \<in> set \<sigma>'. wf\<^sub>t\<^sub>r\<^sub>m t"
    using unify_list_wf_trm[of "[(s,t)]" "[]"] by (auto split: option.splits)
  thus ?thesis
  proof (induction \<sigma>' arbitrary: \<sigma> v rule: List.rev_induct)
    case (snoc x \<sigma>' \<sigma> v)
    def \<theta> \<equiv> "subst_of \<sigma>'"
    hence "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)" using snoc.prems(2) snoc.IH[of \<theta>] by fastforce 
    moreover obtain w t where x: "x = (w,t)" by (metis surj_pair) 
    hence \<sigma>: "\<sigma> = Var(w := t) \<circ>\<^sub>s \<theta>" using snoc.prems(1) by (simp add: subst_def \<theta>_def)
    moreover have "wf\<^sub>t\<^sub>r\<^sub>m t" using snoc.prems(2) x by auto
    ultimately show ?case by (simp add: subst_compose_def wf_trm_subst)
  qed (simp add: wf\<^sub>t\<^sub>r\<^sub>m_def)
qed


subsubsection {* Transparent function decomposition *}
definition transparent::"'fun \<Rightarrow> bool" where
  "transparent f \<equiv> public f \<and> f \<in> \<Sigma>\<^sub>f \<and> (\<forall>X. Ana (Fun f X) = ({},set X))"

definition \<Sigma>\<^sub>t\<^sub>r\<^sub>p where "\<Sigma>\<^sub>t\<^sub>r\<^sub>p \<equiv> {f. transparent f}"
declare \<Sigma>\<^sub>t\<^sub>r\<^sub>p_def[simp]

lemma transp_public[dest]: "transparent f \<Longrightarrow> public f" by (metis transparent_def)
lemma transp_fun[dest]: "transparent f \<Longrightarrow> f \<in> \<Sigma>\<^sub>f" by (metis transparent_def)
lemma transp_Ana[dest]: "transparent f \<Longrightarrow> Ana (Fun f X) = ({},set X)" by (metis transparent_def)

fun trp::"('fun,'var) term \<Rightarrow> ('fun,'var) terms" where
  "trp (Var x) = {Var x}"
| "trp (Fun f X) = insert (Fun f X) (if transparent f then \<Union>x \<in> set X. trp x else {})"

abbreviation trp\<^sub>s\<^sub>e\<^sub>t where "trp\<^sub>s\<^sub>e\<^sub>t S \<equiv> \<Union>(trp ` S)"

abbreviation subterm\<^sub>t\<^sub>r\<^sub>p (infix "\<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p" 50) where "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t' \<equiv> t \<in> trp t'"

lemma finite_trp[simp]: "finite (trp t)" by (induct t rule: trp.induct) auto

lemma trp_refl[simp]: "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t" by (induct t rule: trp.induct) simp_all

lemma trp_subst_apply_subset: "(trp t) \<cdot>set \<delta> \<subseteq> trp (t \<cdot> \<delta>)"
by (induct t, auto)

lemma trp_subterms_subset: "trp t \<subseteq> subterms t"
by (induct t) auto

lemma trpD[dest?]: "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t' \<Longrightarrow> t \<sqsubseteq> t'"
by (induct t' rule: subterms.induct, auto, meson UN_E empty_iff)

lemma trpI[intro?]: "t \<in> M \<Longrightarrow> t \<in> trp\<^sub>s\<^sub>e\<^sub>t M" by fastforce

lemma trpI'[intro?]: "\<lbrakk>transparent f; t \<in> set X\<rbrakk> \<Longrightarrow> t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p Fun f X" by force

lemma trp_mono: "M \<subseteq> M' \<Longrightarrow> trp\<^sub>s\<^sub>e\<^sub>t M \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t M'" by auto

lemma trp_FV_is_trm_FV: "FV\<^sub>s\<^sub>e\<^sub>t (trp t) = FV t" by (induct t) auto

lemma trp_union_FV_is_set_FV: "FV\<^sub>s\<^sub>e\<^sub>t (trp\<^sub>s\<^sub>e\<^sub>t M) = FV\<^sub>s\<^sub>e\<^sub>t M" using trp_FV_is_trm_FV by auto

lemma trp_member_FV: "t \<in> trp\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> FV t \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
by (metis FV\<^sub>s\<^sub>e\<^sub>t_def UN_upper trp_union_FV_is_set_FV)

lemma trp_subst_apply_subset_set: "trp\<^sub>s\<^sub>e\<^sub>t S \<cdot>set \<delta> \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t (S \<cdot>set \<delta>)"
proof
  fix x assume "x \<in> trp\<^sub>s\<^sub>e\<^sub>t S \<cdot>set \<delta>"
  then obtain y z where "trp z \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t S" "x = y \<cdot> \<delta>" "y \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p z" "z \<in> S"
    by auto
  hence "x \<in> trp z \<cdot>set \<delta>" by simp
  hence "x \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p (z \<cdot> \<delta>)" using trp_subst_apply_subset by auto
  thus "x \<in> trp\<^sub>s\<^sub>e\<^sub>t (S \<cdot>set \<delta>)" using \<open>z \<in> S\<close> by auto
qed

lemma trp_fun_member:
  assumes "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p (Fun f X)" "t \<noteq> Fun f X"
  shows "transparent f" "\<exists>x \<in> set X. t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p x"
proof -
  have "t \<notin> {Fun f X}" using assms(2) by simp
  thus "transparent f" using assms(1) by fastforce
  thus "\<exists>x \<in> set X. t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p x" using assms by auto
qed

lemma trp_member_trp_subset: "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t' \<Longrightarrow> trp t \<subseteq> trp t'"
proof (induction t' rule: trp.induct)
  case (2 f X) thus ?case by (cases "transparent f") auto
qed simp

lemma trp_member_trp_subset_union: "t \<in> trp\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> trp t \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t M"
using trp_mono trp_member_trp_subset by fastforce

lemma trp_member_trp_subset_union_subst: "t \<in> trp\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> trp (t \<cdot> \<theta>) \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>)"
using trp_subst_apply_subset_set[of \<theta> M] by (force intro!: trp_member_trp_subset_union)

lemma trp_var_is_FV[dest?]: "Var v \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t \<Longrightarrow> v \<in> FV t"
using trpD vars_iff_subtermeq by metis


subsubsection {* Intruder Deduction Definitions *}
inductive intruder_synth::"('fun,'var) terms \<Rightarrow> ('fun,'var) term \<Rightarrow> bool" (infix "\<turnstile>\<^sub>c" 50)
where
  AxiomC[simp]:   "t \<in> M \<Longrightarrow> M \<turnstile>\<^sub>c t"
| ComposeC[simp]: "\<lbrakk>length X = arity f; public f; \<And>x. x \<in> (set X) \<Longrightarrow> M \<turnstile>\<^sub>c x\<rbrakk> \<Longrightarrow> M \<turnstile>\<^sub>c Fun f X"

inductive intruder_deduct::"('fun,'var) terms \<Rightarrow> ('fun,'var) term \<Rightarrow> bool" (infix "\<turnstile>" 50)
where
  Axiom[simp]:   "t \<in> M \<Longrightarrow> M \<turnstile> t"
| Compose[simp]: "\<lbrakk>length X = arity f; public f; \<And>x. x \<in> set X \<Longrightarrow> M \<turnstile> x\<rbrakk> \<Longrightarrow> M \<turnstile> Fun f X"
| Decompose:     "\<lbrakk>M \<turnstile> t; Ana t = (K, T); \<And>k. k \<in> K \<Longrightarrow> M \<turnstile> k; t\<^sub>i \<in> T\<rbrakk> \<Longrightarrow> M \<turnstile> t\<^sub>i"

definition analyzed::"('fun,'var) terms \<Rightarrow> bool" where
  "analyzed M \<equiv> \<forall>t. M \<turnstile> t \<longleftrightarrow> M \<turnstile>\<^sub>c t"

definition decomp_closure::"('fun,'var) terms \<Rightarrow> ('fun,'var) terms \<Rightarrow> bool" where
  "decomp_closure M M' \<equiv> \<forall>t. M \<turnstile> t \<and> (\<exists>t' \<in> M. t \<sqsubseteq> t') \<longleftrightarrow> t \<in> M'"

inductive public_ground_wf_term::"('fun,'var) term \<Rightarrow> bool" where
  PGWT[simp]: "\<lbrakk>public f; arity f = length X;
                \<And>x. x \<in> set X \<Longrightarrow> public_ground_wf_term x\<rbrakk>
                  \<Longrightarrow> public_ground_wf_term (Fun f X)"

abbreviation "public_ground_wf_terms \<equiv> {t. public_ground_wf_term t}"

lemma pgwt_infinite: "infinite public_ground_wf_terms"
proof -
  let ?F = "(\<lambda>c. Fun c []) ` \<C>\<^sub>p\<^sub>u\<^sub>b"
  have "\<exists>f. bij_betw f \<C>\<^sub>p\<^sub>u\<^sub>b ?F" using bij_betwI'[of \<C>\<^sub>p\<^sub>u\<^sub>b _ ?F] by fastforce
  hence "infinite ?F" by (metis bij_betw_finite infinite_fun_syms(3))
  moreover have "?F \<subseteq> public_ground_wf_terms"
    using \<C>pub_unfold public_ground_wf_term.intros[of _ "[]"]
    by fastforce
  ultimately show ?thesis using infinite_super by blast
qed

declare analyzed_def[simp]
declare decomp_closure_def[simp]

lemma public_const_deduct:
  assumes "c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b"
  shows "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
proof -
  have "arity c = 0" "public c" using const_arity_eq_zero \<open>c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b\<close> by auto
  thus "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
    using intruder_synth.ComposeC[OF _ \<open>public c\<close>, of "[]"]
          intruder_deduct.Compose[OF _ \<open>public c\<close>, of "[]"]
    by auto
qed

lemma public_const_deduct'[simp]:
  assumes "arity c = 0" "public c"
  shows "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
using intruder_deduct.Compose[of "[]" c] intruder_synth.ComposeC[of "[]" c] assms by simp_all

lemma pgwt_public: "\<lbrakk>public_ground_wf_term t; Fun f X \<sqsubseteq> t\<rbrakk> \<Longrightarrow> public f"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_ground: "public_ground_wf_term t \<Longrightarrow> FV t = {}"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_fun: "public_ground_wf_term t \<Longrightarrow> \<exists>f X. t = Fun f X"
using pgwt_ground[of t] by (cases t) auto

lemma pgwt_arity: "\<lbrakk>public_ground_wf_term t; Fun f X \<sqsubseteq> t\<rbrakk> \<Longrightarrow> arity f = length X"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_wellformed: "public_ground_wf_term t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_deducible: "public_ground_wf_term t \<Longrightarrow> M \<turnstile>\<^sub>c t"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_is_empty_synth: "public_ground_wf_term t \<longleftrightarrow> {} \<turnstile>\<^sub>c t"
proof -
  { fix M::"('fun,'var) term set" assume "M \<turnstile>\<^sub>c t" "M = {}" hence "public_ground_wf_term t"
      by (induct t rule: intruder_synth.induct) auto
  }
  thus ?thesis using pgwt_deducible by auto
qed

lemma trp_deduct_decompose:
  assumes "s \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t" "M \<turnstile> t"
  shows "M \<turnstile> s"
using assms
proof (induction t rule: trp.induct)
  case (2 f X) thus ?case
  proof (cases "s = Fun f X")
    case False
    then obtain x where x: "transparent f" "x \<in> set X" "s \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p x"
      using "2.prems"(1) trp_fun_member by blast
    hence "Ana (Fun f X) = ({},set X)" unfolding transparent_def by auto
    hence "M \<turnstile> x" using Decompose[OF \<open>M \<turnstile> Fun f X\<close> _ _ \<open>x \<in> set X\<close>] by auto
    thus ?thesis using "2.IH"[OF x] by metis
  qed simp
qed simp

lemma trp_deduct_decompose':
  assumes "trp\<^sub>s\<^sub>e\<^sub>t M \<turnstile> t" shows "M \<turnstile> t"
proof -
  { fix M' assume "M' \<turnstile> t" "M' = trp\<^sub>s\<^sub>e\<^sub>t M" hence "M \<turnstile> t"
    proof (induction t rule: intruder_deduct.induct)
      case (Decompose M' t K T t')
      hence "\<And>k. k \<in> K \<Longrightarrow> M \<turnstile> k" "M \<turnstile> t" by auto
      thus ?case using intruder_deduct.Decompose[of M t K T] \<open>Ana t = (K, T)\<close> \<open>t' \<in> T\<close> by metis
    qed (auto simp add: trp_deduct_decompose)
  }
  thus ?thesis using assms by simp
qed

lemma ideduct_synth_subst_apply:
  assumes "{} \<turnstile>\<^sub>c t" "\<And>v. M \<turnstile>\<^sub>c \<theta> v"
  shows "M \<turnstile>\<^sub>c t \<cdot> \<theta>"
proof -
  { fix M'::"('fun,'var) term set" assume "M' \<turnstile>\<^sub>c t" "M' = {}" hence "M \<turnstile>\<^sub>c t \<cdot> \<theta>"
    proof (induction t rule: intruder_synth.induct)
      case (ComposeC X f M')
      hence "length (map (\<lambda>t. t \<cdot> \<theta>) X) = arity f" "\<And>x. x \<in> set (map (\<lambda>t. t \<cdot> \<theta>) X) \<Longrightarrow> M \<turnstile>\<^sub>c x"
        by auto
      thus ?case using intruder_synth.ComposeC[of "map (\<lambda>t. t \<cdot> \<theta>) X" f M] \<open>public f\<close> by fastforce
    qed simp
  }
  thus ?thesis using assms by metis
qed


subsubsection {* Specialized induction rules that do not quantify over the intruder knowledge *}
lemma intruder_deduct_induct[consumes 1, case_names Axiom Compose Decompose]:
  assumes "M \<turnstile> t" "\<And>t. t \<in> M \<Longrightarrow> P M t"
          "\<And>X f. \<lbrakk>length X = arity f; public f;
                  \<And>x. x \<in> set X \<Longrightarrow> M \<turnstile> x;
                  \<And>x. x \<in> set X \<Longrightarrow> P M x\<rbrakk> \<Longrightarrow> P M (Fun f X)"
          "\<And>t K T t\<^sub>i. \<lbrakk>M \<turnstile> t; P M t; Ana t = (K, T); \<And>k. k \<in> K \<Longrightarrow> M \<turnstile> k;
                       \<And>k. k \<in> K \<Longrightarrow> P M k; t\<^sub>i \<in> T\<rbrakk> \<Longrightarrow> P M t\<^sub>i"
  shows "P M t"
using assms by (induct rule: intruder_deduct.induct) blast+

lemma intruder_synth_induct[consumes 1, case_names AxiomC ComposeC]:
  assumes "M \<turnstile>\<^sub>c t" "\<And>t. t \<in> M \<Longrightarrow> P M t"
          "\<And>X f. \<lbrakk>length X = arity f; public f;
                  \<And>x. x \<in> set X \<Longrightarrow> M \<turnstile>\<^sub>c x;
                  \<And>x. x \<in> set X \<Longrightarrow> P M x\<rbrakk> \<Longrightarrow> P M (Fun f X)"
  shows "P M t"
using assms by (induct rule: intruder_synth.induct) auto
  

subsubsection {* Monotonicity lemmas *}
lemma ideduct_mono:
  "\<lbrakk>M \<turnstile> t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> M' \<turnstile> t"
proof (induction rule: intruder_deduct.induct)
  case (Decompose M t K T t\<^sub>i)
  have "\<forall>k. k \<in> K \<longrightarrow> M' \<turnstile> k" using Decompose.IH \<open>M \<subseteq> M'\<close> by simp
  moreover have "M' \<turnstile> t" using Decompose.IH \<open>M \<subseteq> M'\<close> by simp
  ultimately show ?case using Decompose.hyps intruder_deduct.Decompose by blast
qed auto

lemma ideduct_synth_mono:
  "\<lbrakk>M \<turnstile>\<^sub>c t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> M' \<turnstile>\<^sub>c t"
by (induct rule: intruder_synth.induct) auto

lemma (in intruder_model) ideduct_reduce:
  "\<lbrakk>M \<union> M' \<turnstile> t; \<And>t'. t' \<in> M' \<Longrightarrow> M \<turnstile> t'\<rbrakk> \<Longrightarrow> M \<turnstile> t"
proof (induction rule: intruder_deduct_induct)
  case Decompose thus ?case using intruder_deduct.Decompose by blast 
qed auto

lemma ideduct_synth_reduce:
  "\<lbrakk>M \<union> M' \<turnstile>\<^sub>c t; \<And>t'. t' \<in> M' \<Longrightarrow> M \<turnstile>\<^sub>c t'\<rbrakk> \<Longrightarrow> M \<turnstile>\<^sub>c t"
by (induct rule: intruder_synth_induct) auto

lemma ideduct_ik_eq: assumes "\<forall>t \<in> M. M' \<turnstile> t" shows "M' \<turnstile> t \<longleftrightarrow> M' \<union> M \<turnstile> t"
by (meson assms ideduct_mono ideduct_reduce sup_ge1)

lemma ideduct_mono_eq:
  assumes "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile> t" shows "M \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<turnstile> t"
proof
  show "M \<union> N \<turnstile> t \<Longrightarrow> M' \<union> N \<turnstile> t"
  proof (induction t rule: intruder_deduct_induct)
    case (Axiom t) thus ?case
    proof (cases "t \<in> M")
      case True
      hence "M \<turnstile> t" using intruder_deduct.Axiom by metis
      thus ?thesis using assms ideduct_mono[of M' t "M' \<union> N"] by simp
    qed auto
  next
    case (Compose X f) thus ?case using intruder_deduct.Compose by auto
  next
    case (Decompose t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M' \<union> N" t K T] by auto
  qed

  show "M' \<union> N \<turnstile> t \<Longrightarrow> M \<union> N \<turnstile> t"
  proof (induction t rule: intruder_deduct_induct)
    case (Axiom t) thus ?case
    proof (cases "t \<in> M'")
      case True
      hence "M' \<turnstile> t" using intruder_deduct.Axiom by metis
      thus ?thesis using assms ideduct_mono[of M t "M \<union> N"] by simp
    qed auto
  next
    case (Compose X f) thus ?case using intruder_deduct.Compose by auto
  next
    case (Decompose t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M \<union> N" t K T] by auto
  qed
qed

lemma deduct_synth_subterm:
  assumes "M \<turnstile>\<^sub>c t" "s \<in> subterms t" "\<forall>m \<in> M. \<forall>s \<in> subterms m. M \<turnstile>\<^sub>c s"
  shows "M \<turnstile>\<^sub>c s"
using assms by (induct t rule: intruder_synth.induct) auto

lemma deduct_if_synth[intro, dest]: "M \<turnstile>\<^sub>c t \<Longrightarrow> M \<turnstile> t"
by (induct rule: intruder_synth.induct) auto

lemma synth_if_deduct_empty: "{} \<turnstile> t \<Longrightarrow> {} \<turnstile>\<^sub>c t"
proof (induction t rule: intruder_deduct_induct)
  case (Decompose t K M m)
  then obtain f T where "t = Fun f T" "m \<in> set T"
    using Ana_fun_subterm Ana_var by (cases t) fastforce+
  with Decompose.IH(1) show ?case by (induction rule: intruder_synth_induct) auto
qed auto

lemma ideduct_deduct_synth_mono_eq:
  assumes "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile>\<^sub>c t" "M \<subseteq> M'"
  and "\<forall>t. M' \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<union> D \<turnstile>\<^sub>c t"
  shows "M \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<union> D \<turnstile>\<^sub>c t"
proof -
  have "\<forall>m \<in> M'. M \<turnstile> m" using assms(1) by auto
  hence "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile> t" by (metis assms(1,2) deduct_if_synth ideduct_reduce sup.absorb2)
  hence "\<forall>t. M' \<union> N \<turnstile> t \<longleftrightarrow> M \<union> N \<turnstile> t" by (meson ideduct_mono_eq)
  thus ?thesis by (meson assms(3))
qed

lemma deduct_if_trp_synth: "trp\<^sub>s\<^sub>e\<^sub>t M \<turnstile>\<^sub>c t \<Longrightarrow> M \<turnstile> t"
using deduct_if_synth trp_deduct_decompose' by metis

lemma ideduct_subst: "M \<turnstile> t \<Longrightarrow> M \<cdot>set \<delta> \<turnstile> t \<cdot> \<delta>"
proof (induction t rule: intruder_deduct_induct)
  case (Compose T f)
  hence "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f" "\<And>t. t \<in> set T \<Longrightarrow> M \<cdot>set \<delta> \<turnstile> t \<cdot> \<delta>" by auto
  thus ?case using intruder_deduct.Compose[OF _ Compose.hyps(2), of "map (\<lambda>t. t \<cdot> \<delta>) T"] by auto
next
  case (Decompose t K M' m')
  hence "Ana (t \<cdot> \<delta>) = (K \<cdot>set \<delta>, M' \<cdot>set \<delta>)" "\<And>k. k \<in> K \<cdot>set \<delta> \<Longrightarrow> M \<cdot>set \<delta> \<turnstile> k" "m' \<cdot> \<delta> \<in> M' \<cdot>set \<delta>"
    using Ana_subst[OF Decompose.hyps(2)] by auto
  thus ?case using intruder_deduct.Decompose[OF Decompose.IH(1)] by metis
qed simp

lemma ideduct_synth_subst: "M \<turnstile>\<^sub>c t \<Longrightarrow> M \<cdot>set \<delta> \<turnstile>\<^sub>c t \<cdot> \<delta>"
proof (induction t rule: intruder_synth_induct)
  case (ComposeC T f)
  hence "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f" "\<And>t. t \<in> set T \<Longrightarrow> M \<cdot>set \<delta> \<turnstile>\<^sub>c t \<cdot> \<delta>" by auto
  thus ?case using intruder_synth.ComposeC[OF _ ComposeC.hyps(2), of "map (\<lambda>t. t \<cdot> \<delta>) T"] by auto
qed simp

lemma ideduct_vars:
  assumes "M \<turnstile> t"
  shows "FV t \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
using assms
proof (induction t rule: intruder_deduct_induct)
  case (Decompose t K T t\<^sub>i) thus ?case
    using Ana_vars(2) FV_subset by blast 
qed auto

lemma ideduct_synth_vars:
  assumes "M \<turnstile>\<^sub>c t"
  shows "FV t \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
using assms by (induct t rule: intruder_synth_induct) auto


subsubsection {* Intruder knowledge closure theorem *}
lemma deducts_eq_if_analyzed: "analyzed M \<Longrightarrow> M \<turnstile> t \<longleftrightarrow> M \<turnstile>\<^sub>c t"
by auto

lemma closure_is_superset: "decomp_closure M M' \<Longrightarrow> M \<subseteq> M'"
by force

lemma deduct_if_closure_deduct: "\<lbrakk>M' \<turnstile> t; decomp_closure M M'\<rbrakk> \<Longrightarrow> M \<turnstile> t"
proof (induction t rule: intruder_deduct.induct)
  case (Decompose M' t K T t\<^sub>i)
  thus ?case using intruder_deduct.Decompose[OF _ \<open>Ana t = (K,T)\<close> _ \<open>t\<^sub>i \<in> T\<close>] by simp
qed auto

lemma deduct_if_closure_synth: "\<lbrakk>decomp_closure M M'; M' \<turnstile>\<^sub>c t\<rbrakk> \<Longrightarrow> M \<turnstile> t"
using deduct_if_closure_deduct by blast

lemma closure_subterms_composable:
  assumes "decomp_closure M M'"
  and "M' \<turnstile>\<^sub>c t'" "M' \<turnstile> t" "t \<sqsubseteq> t'"
  shows "M' \<turnstile>\<^sub>c t"
using \<open>M' \<turnstile>\<^sub>c t'\<close> assms
proof (induction t' rule: intruder_synth.induct)
  case (AxiomC t' M')
  have "M \<turnstile> t" using \<open>M' \<turnstile> t\<close> deduct_if_closure_deduct AxiomC.prems(1) by blast
  moreover
  { have "\<exists>s \<in> M. t' \<sqsubseteq> s" using \<open>t' \<in> M'\<close> AxiomC.prems(1) unfolding decomp_closure_def by blast
    hence "\<exists>s \<in> M. t \<sqsubseteq> s" using \<open>t \<sqsubseteq> t'\<close> subtermeq_trans by auto
  }
  ultimately have "t \<in> M'" using AxiomC.prems(1) unfolding decomp_closure_def by blast
  thus ?case by simp
next
  case (ComposeC X f M')
  let ?t' = "Fun f X"
  { assume "t = ?t'" have "M' \<turnstile>\<^sub>c t" using \<open>M' \<turnstile>\<^sub>c ?t'\<close> \<open>t = ?t'\<close> by simp }
  moreover
  { assume "t \<noteq> ?t'"
    have "\<exists>x \<in> set X. t \<sqsubseteq> x" using \<open>t \<sqsubseteq> ?t'\<close> \<open>t \<noteq> ?t'\<close> by simp
    hence "M' \<turnstile>\<^sub>c t" using ComposeC.IH ComposeC.prems(1,3) ComposeC.hyps(3) by blast
  }
  ultimately show ?case using cases_simp[of "t = ?t'" "M' \<turnstile>\<^sub>c t"] by simp
qed

lemma closure_analyzed:
  assumes "decomp_closure M M'"
  shows "analyzed M'"
proof -
  { fix t assume "M' \<turnstile> t" have "M' \<turnstile>\<^sub>c t" using \<open>M' \<turnstile> t\<close> assms
    proof (induction t rule: intruder_deduct.induct)
      case (Decompose M' t K T t\<^sub>i) 
      hence "M' \<turnstile> t\<^sub>i" using Decompose.hyps intruder_deduct.Decompose by blast
      moreover have "t\<^sub>i \<sqsubseteq> t"
        using Decompose.hyps(4) Ana_subterm[OF Decompose.hyps(2)] unfolding subtermeq_def by blast
      moreover have "M' \<turnstile>\<^sub>c t" using Decompose.IH(1) Decompose.prems by blast
      ultimately show "M' \<turnstile>\<^sub>c t\<^sub>i" using closure_subterms_composable Decompose.prems by blast
    qed auto
  }
  moreover have "\<forall>t. M \<turnstile>\<^sub>c t \<longrightarrow> M \<turnstile> t" by auto
  ultimately show ?thesis by auto
qed

lemma ik_has_synth_ik_closure:
  fixes M :: "('fun,'var) terms"
  shows "\<exists>M'. (\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile>\<^sub>c t) \<and> decomp_closure M M' \<and> (finite M \<longrightarrow> finite M')"
proof -
  let ?M' = "{t. M \<turnstile> t \<and> (\<exists>t' \<in> M. t \<sqsubseteq> t')}"

  have M'_closes: "decomp_closure M ?M'" by simp
  hence "M \<subseteq> ?M'" using closure_is_superset by simp

  have "\<forall>t. ?M' \<turnstile>\<^sub>c t \<longrightarrow> M \<turnstile> t" using deduct_if_closure_synth[OF M'_closes] by blast 
  moreover have "\<forall>t. M \<turnstile> t \<longrightarrow> ?M' \<turnstile> t" using ideduct_mono[OF _ \<open>M \<subseteq> ?M'\<close>] by simp
  moreover have "analyzed ?M'" using closure_analyzed[OF M'_closes] .
  ultimately have "\<forall>t. M \<turnstile> t \<longleftrightarrow> ?M' \<turnstile>\<^sub>c t" unfolding analyzed_def by blast
  moreover have "finite M \<longrightarrow> finite ?M'" by auto
  ultimately show ?thesis using M'_closes by blast
qed


subsubsection {* Transparently analysable subterms can be inferred without decomposition *}
lemma trp_subterm_synth_deduct:
  assumes "trp\<^sub>s\<^sub>e\<^sub>t M \<turnstile>\<^sub>c t" "s \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t"
  shows "trp\<^sub>s\<^sub>e\<^sub>t M \<turnstile>\<^sub>c s"
using assms
proof (induction t rule: intruder_synth_induct)
  case (AxiomC t)
  hence "s \<in> trp\<^sub>s\<^sub>e\<^sub>t M" using trp_member_trp_subset_union[of t M] by auto
  thus ?case by simp
next
  case (ComposeC X f) thus ?case
  proof (cases "s = Fun f X")
    case False
    hence "transparent f" using \<open>s \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p (Fun f X)\<close> using trp_fun_member(1) by blast 
    then obtain x where "x \<in> set X" "s \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p x" using \<open>s \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p (Fun f X)\<close> \<open>s \<noteq> Fun f X\<close> by auto
    thus ?thesis using ComposeC.IH by metis
  qed simp
qed


subsubsection {* Lemmas concerning transparent function decomposition with substitutions *}
lemma var_in_trp_if_in_subst_diff:
  assumes "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t' \<cdot> \<sigma>" "t \<notin> trp t' \<cdot>set \<sigma>"
  shows "\<exists>v. Var v \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t' \<and> t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p \<sigma> v"
using assms
proof (induction t')
  case (Fun f X)
  hence "t \<noteq> Fun f X \<cdot> \<sigma>" using subst_all_member trp_refl by blast

  have "transparent f"
  proof (rule ccontr)
    assume "\<not>transparent f"
    hence "trp (Fun f X \<cdot> \<sigma>) = {Fun f X \<cdot> \<sigma>}" by simp
    thus False using \<open>t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p Fun f X \<cdot> \<sigma>\<close> \<open>t \<noteq> Fun f X \<cdot> \<sigma>\<close> by auto
  qed 

  have trp_unfold: "trp (Fun f X) = insert (Fun f X) (UNION (set X) trp)"
    using \<open>transparent f\<close> by simp
  hence *: "\<forall>x \<in> set X. t \<notin> trp x \<cdot>set \<sigma>"
    using \<open>t \<notin> trp (Fun f X) \<cdot>set \<sigma>\<close> subst_all_mono[of _ "trp (Fun f X)" \<sigma>] by auto
  
  have **: "\<exists>x \<in> set X. t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p x \<cdot> \<sigma>" using \<open>t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p Fun f X \<cdot> \<sigma>\<close> \<open>t \<noteq> Fun f X \<cdot> \<sigma>\<close>
    by (auto simp add: \<open>transparent f\<close>)

  from * ** obtain x where x: "x \<in> set X" "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p x \<cdot> \<sigma>" "t \<notin> trp x \<cdot>set \<sigma>" by auto
  hence "\<exists>v. Var v \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p x \<and> t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p (\<sigma> v)" using Fun.IH by metis
  thus ?case using \<open>x \<in> set X\<close> trp_unfold by auto
qed simp

lemma var_in_trp_if_in_subst_diff_set:
  assumes "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<sigma>)" "t \<notin> (trp\<^sub>s\<^sub>e\<^sub>t M) \<cdot>set \<sigma>"
  shows "\<exists>v. Var v \<in> trp\<^sub>s\<^sub>e\<^sub>t M \<and> t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p \<sigma> v \<and> t \<noteq> \<sigma> v"
proof -
  from assms(1) obtain t' where t': "t' \<in> M" "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t' \<cdot> \<sigma>" by auto
  hence "t' \<in> trp\<^sub>s\<^sub>e\<^sub>t M" by fastforce
  hence "trp t' \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t M" using \<open>t' \<in> M\<close> by blast 
  hence "trp t' \<cdot>set \<sigma> \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t M \<cdot>set \<sigma>" by (simp add: subst_all_mono)
  hence "t \<notin> trp t' \<cdot>set \<sigma>" using assms(2) by auto
  then obtain v where "Var v \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t'" "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p \<sigma> v"
    using var_in_trp_if_in_subst_diff[OF t'(2)] by metis
  hence "Var v \<in> trp\<^sub>s\<^sub>e\<^sub>t M" using \<open>t' \<in> trp\<^sub>s\<^sub>e\<^sub>t M\<close> \<open>t' \<in> M\<close> by blast
  thus ?thesis
    using subst_all_member[OF \<open>Var v \<in> trp\<^sub>s\<^sub>e\<^sub>t M\<close>, of \<sigma>] \<open>t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p \<sigma> v\<close> \<open>t \<notin> trp\<^sub>s\<^sub>e\<^sub>t M \<cdot>set \<sigma>\<close>
    by auto
qed

lemma trp_subst_union_unfold:
  "trp\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>) = (trp\<^sub>s\<^sub>e\<^sub>t M \<cdot>set \<theta>) \<union> \<Union>{trp (\<theta> v) | v. Var v \<in> trp\<^sub>s\<^sub>e\<^sub>t M}"
proof
  let ?A = "trp\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>)"
  let ?B = "trp\<^sub>s\<^sub>e\<^sub>t M \<cdot>set \<theta>"
  let ?C = "\<Union>{trp (\<theta> v) | v. Var v \<in> trp\<^sub>s\<^sub>e\<^sub>t M}"

  show "?B \<union> ?C \<subseteq> ?A"
  proof -
    have "?B \<subseteq> ?A" using trp_subst_apply_subset_set by metis
    moreover have "?C \<subseteq> ?A"
    proof
      fix t assume "t \<in> ?C"
      then obtain v where "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p (\<theta> v)" "Var v \<in> trp\<^sub>s\<^sub>e\<^sub>t M" by auto
      thus "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (M \<cdot>set \<theta>)"
        using trp_member_trp_subset_union_subst[of "Var v" M \<theta>] by auto
    qed
    ultimately show ?thesis by simp
  qed

  show "?A \<subseteq> ?B \<union> ?C"
  proof
    fix t assume "t \<in> ?A"
    thus "t \<in> ?B \<union> ?C"
    proof (cases "t \<in> ?B")
      case False
      then obtain v where "Var v \<in> trp\<^sub>s\<^sub>e\<^sub>t M" "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p (\<theta> v)"
        using var_in_trp_if_in_subst_diff_set \<open>t \<in> ?A\<close> by metis
      hence "t \<in> ?C" by blast
      thus "t \<in> ?B \<union> ?C" by auto
    qed auto
  qed
qed

end

end
