Theory Typed_Model
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. wf⇩t⇩r⇩m (Γ (Var x))"
begin
subsection ‹Definitions›
text ‹The set of atomic types›
abbreviation "𝔗⇩a ≡ UNIV::('atom set)"
text ‹Well-typed substitutions›
definition wt⇩s⇩u⇩b⇩s⇩t where
"wt⇩s⇩u⇩b⇩s⇩t σ ≡ (∀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; wt⇩s⇩u⇩b⇩s⇩t δ; wf⇩t⇩r⇩m⇩s (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 tfr⇩s⇩e⇩t where
"tfr⇩s⇩e⇩t 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 tfr⇩s⇩t⇩p where
"tfr⇩s⇩t⇩p (Equality a t t') = ((∃δ. Unifier δ t t') ⟶ Γ t = Γ t')"
| "tfr⇩s⇩t⇩p (Inequality X F) = (
(∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X. ∃a. Γ (Var x) = TAtom a) ∨
(∀f T. Fun f T ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F) ⟶ T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X)))"
| "tfr⇩s⇩t⇩p _ = 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 tfr⇩s⇩t where
"tfr⇩s⇩t S ≡ tfr⇩s⇩e⇩t (trms⇩s⇩t S) ∧ list_all tfr⇩s⇩t⇩p S"
subsection ‹Small Lemmata›
lemma tfr⇩s⇩t⇩p_list_all_alt_def:
"list_all tfr⇩s⇩t⇩p S ⟷
((∀a t t'. Equality a t t' ∈ set S ∧ (∃δ. Unifier δ t t') ⟶ Γ t = Γ t') ∧
(∀X F. Inequality X F ∈ set S ⟶
(∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X. ∃a. Γ (Var x) = TAtom a)
∨ (∀f T. Fun f T ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s 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': "wf⇩t⇩r⇩m t ⟹ wf⇩t⇩r⇩m (Γ t)"
proof (induction t)
case (Fun f T)
hence *: "arity f = length T" "⋀t. t ∈ set T ⟹ wf⇩t⇩r⇩m (Γ t)" unfolding wf⇩t⇩r⇩m_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" "wf⇩t⇩r⇩m t" shows "arity f = length T"
using Γ_wf'[OF assms(2)] assms(1) unfolding wf⇩t⇩r⇩m_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 "wf⇩t⇩r⇩m (Fun c X)" shows "X = []"
by (metis assms const_type_inv length_0_conv subtermeqI' wf⇩t⇩r⇩m_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]: "wt⇩s⇩u⇩b⇩s⇩t Var" by (metis wt⇩s⇩u⇩b⇩s⇩t_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': "⟦wt⇩s⇩u⇩b⇩s⇩t σ; Γ s = Γ t⟧ ⟹ Γ (s ⋅ σ) = Γ (t ⋅ σ)"
by (metis wt_subst_trm wt⇩s⇩u⇩b⇩s⇩t_def)
lemma wt_subst_trm'': "wt⇩s⇩u⇩b⇩s⇩t σ ⟹ Γ t = Γ (t ⋅ σ)"
by (metis wt_subst_trm wt⇩s⇩u⇩b⇩s⇩t_def)
lemma wt_subst_compose:
assumes "wt⇩s⇩u⇩b⇩s⇩t θ" "wt⇩s⇩u⇩b⇩s⇩t δ" shows "wt⇩s⇩u⇩b⇩s⇩t (θ ∘⇩s δ)"
proof -
have "⋀v. Γ (θ v) = Γ (θ v ⋅ δ)" using wt_subst_trm ‹wt⇩s⇩u⇩b⇩s⇩t δ› unfolding wt⇩s⇩u⇩b⇩s⇩t_def by metis
moreover have "⋀v. Γ (Var v) = Γ (θ v)" using ‹wt⇩s⇩u⇩b⇩s⇩t θ› unfolding wt⇩s⇩u⇩b⇩s⇩t_def by metis
ultimately have "⋀v. Γ (Var v) = Γ (θ v ⋅ δ)" by metis
thus ?thesis unfolding wt⇩s⇩u⇩b⇩s⇩t_def subst_compose_def by metis
qed
lemma wt_subst_TAtom_Var_cases:
assumes θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (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 "wf⇩t⇩r⇩m (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 θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "∀x. wf⇩t⇩r⇩m (θ x)"
and "∀x ∈ fv t - X. ∃a. Γ (Var x) = TAtom a"
shows "∀x ∈ fv (t ⋅ θ) - fv⇩s⇩e⇩t (θ ` 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" "wf⇩t⇩r⇩m (θ x)" using θ unfolding wt⇩s⇩u⇩b⇩s⇩t_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 wf⇩t⇩r⇩m_def by auto
thus ?thesis using Fun by auto
qed
qed auto
qed fastforce
lemma wt_subst_TAtom_subterms_subst:
assumes "wt⇩s⇩u⇩b⇩s⇩t θ" "∀x ∈ fv t. ∃a. Γ (Var x) = TAtom a" "wf⇩t⇩r⇩m⇩s (θ ` fv t)"
shows "subterms (t ⋅ θ) = subterms t ⋅⇩s⇩e⇩t θ"
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 ⋅⇩s⇩e⇩t θ" 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 "wt⇩s⇩u⇩b⇩s⇩t θ" "∀x ∈ fv⇩s⇩e⇩t M. ∃a. Γ (Var x) = TAtom a" "wf⇩t⇩r⇩m⇩s (θ ` fv⇩s⇩e⇩t M)"
shows "subterms⇩s⇩e⇩t (M ⋅⇩s⇩e⇩t θ) = subterms⇩s⇩e⇩t M ⋅⇩s⇩e⇩t θ"
proof
show "subterms⇩s⇩e⇩t (M ⋅⇩s⇩e⇩t θ) ⊆ subterms⇩s⇩e⇩t M ⋅⇩s⇩e⇩t θ"
proof
fix t assume "t ∈ subterms⇩s⇩e⇩t (M ⋅⇩s⇩e⇩t θ)"
then obtain s where s: "s ∈ M" "t ∈ subterms (s ⋅ θ)" by auto
thus "t ∈ subterms⇩s⇩e⇩t M ⋅⇩s⇩e⇩t θ"
using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
by auto
qed
show "subterms⇩s⇩e⇩t M ⋅⇩s⇩e⇩t θ ⊆ subterms⇩s⇩e⇩t (M ⋅⇩s⇩e⇩t θ)"
proof
fix t assume "t ∈ subterms⇩s⇩e⇩t M ⋅⇩s⇩e⇩t θ"
then obtain s where s: "s ∈ M" "t ∈ subterms s ⋅⇩s⇩e⇩t θ" by auto
thus "t ∈ subterms⇩s⇩e⇩t (M ⋅⇩s⇩e⇩t θ)"
using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
by auto
qed
qed
lemma wt_subst_subst_upd:
assumes "wt⇩s⇩u⇩b⇩s⇩t θ"
and "Γ (Var x) = Γ t"
shows "wt⇩s⇩u⇩b⇩s⇩t (θ(x := t))"
using assms unfolding wt⇩s⇩u⇩b⇩s⇩t_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 δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (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 "wf⇩t⇩r⇩m (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 "wf⇩t⇩r⇩m 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 "wf⇩t⇩r⇩m t" "Γ t = TAtom τ"
shows "(∃v. t = Var v) ∨ (∃f. t = Fun f [])"
using assms const_type_inv unfolding wf⇩t⇩r⇩m_def by (cases t) auto
lemma subtermeq_imp_subtermtypeeq:
assumes "wf⇩t⇩r⇩m 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 "wf⇩t⇩r⇩m 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 wf⇩t⇩r⇩m_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 "wf⇩t⇩r⇩m 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]: "wf⇩t⇩r⇩m (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 ‹wf⇩t⇩r⇩m (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 "wt⇩s⇩u⇩b⇩s⇩t θ"
and "wf⇩t⇩r⇩m (θ 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_fv⇩s⇩e⇩t_termtype_subterm:
assumes "x ∈ fv⇩s⇩e⇩t (θ ` Y)"
and "wt⇩s⇩u⇩b⇩s⇩t θ"
and "wf⇩t⇩r⇩m⇩s (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: "wf⇩t⇩r⇩m 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 wf⇩t⇩r⇩m_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: "wf⇩t⇩r⇩m⇩s M"
and f: "arity f > 0"
shows "f ∈ ⋃(funs_term ` Γ ` M) ⟷
(f ∈ ⋃(funs_term ` M) ∨ (∃x ∈ fv⇩s⇩e⇩t M. f ∈ funs_term (Γ (Var x))))" (is "?A ⟷ ?B")
proof
assume ?A
then obtain t where "t ∈ M" "wf⇩t⇩r⇩m 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" "wf⇩t⇩r⇩m 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 "wf⇩t⇩r⇩m 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 "wf⇩t⇩r⇩m t" "Γ t = TAtom τ"
shows "subterms t = {t}"
using assms const_type_inv unfolding wf⇩t⇩r⇩m_def by (cases t) force+
lemma wf_trm_TComp_subterm:
assumes "wf⇩t⇩r⇩m 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 ‹wf⇩t⇩r⇩m s› ‹s = Fun g S› term.order_refl wf⇩t⇩r⇩m_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" "wt⇩s⇩u⇩b⇩s⇩t δ" "t ⊑ s ⋅ δ" "⋀v. wf⇩t⇩r⇩m (δ 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" "wf⇩t⇩r⇩m⇩s M"
shows "wf⇩t⇩r⇩m 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 ∈ ik⇩s⇩t S ⟹ t ∈ SMP (trms⇩s⇩t S)" by force
lemma MP_setI[intro]: "x ∈ set S ⟹ trms⇩s⇩t⇩p x ⊆ trms⇩s⇩t S" by force
lemma SMP_setI[intro]: "x ∈ set S ⟹ trms⇩s⇩t⇩p x ⊆ SMP (trms⇩s⇩t S)" by force
lemma SMP_subset_I:
assumes M: "∀t ∈ M. ∃s δ. s ∈ N ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (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" "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (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 (trms⇩s⇩t (S@S')) = SMP (trms⇩s⇩t S) ∪ SMP (trms⇩s⇩t 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 (⋃m∈M. f m) ⊆ (⋃m∈M. SMP (f m))"
proof
fix t assume "t ∈ SMP (⋃m∈M. f m)"
thus "t ∈ (⋃m∈M. SMP (f m))" by (induct t rule: SMP.induct) force+
qed
show "(⋃m∈M. SMP (f m)) ⊆ SMP (⋃m∈M. f m)"
proof
fix t assume "t ∈ (⋃m∈M. SMP (f m))"
then obtain m where "m ∈ M" "t ∈ SMP (f m)" by atomize_elim auto
thus "t ∈ SMP (⋃m∈M. f m)" using SMP_mono[of "f m" "⋃m∈M. 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 (trms⇩s⇩t (x#S)) = SMP (trms⇩s⇩t [x]) ∪ SMP (trms⇩s⇩t S)"
using SMP_append[of "[x]" S] by auto
lemma SMP_Nil[simp]: "SMP (trms⇩s⇩t []) = {}"
proof -
{ fix t assume "t ∈ SMP (trms⇩s⇩t [])" 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: "subterms⇩s⇩e⇩t M ⊆ SMP M"
proof
fix t assume "t ∈ subterms⇩s⇩e⇩t 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: "wt⇩s⇩u⇩b⇩s⇩t δ ⟹ wt⇩s⇩u⇩b⇩s⇩t (rm_vars X δ)"
using rm_vars_dom unfolding wt⇩s⇩u⇩b⇩s⇩t_def by auto
lemma wt_subst_SMP_subset:
assumes "trms⇩s⇩t S ⊆ SMP S'" "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "trms⇩s⇩t (S ⋅⇩s⇩t δ) ⊆ SMP S'"
proof
fix t assume *: "t ∈ trms⇩s⇩t (S ⋅⇩s⇩t δ)"
show "t ∈ SMP S'" using trm_strand_subst_cong(2)[OF *]
proof
assume "∃t'. t = t' ⋅ δ ∧ t' ∈ trms⇩s⇩t S"
thus "t ∈ SMP S'" using assms SMP.Substitution by auto
next
assume "∃X F. Inequality X F ∈ set S ∧ (∃t'∈trms⇩p⇩a⇩i⇩r⇩s F. t = t' ⋅ rm_vars (set X) δ)"
then obtain X F t' where **:
"Inequality X F ∈ set S" "t'∈trms⇩p⇩a⇩i⇩r⇩s F" "t = t' ⋅ rm_vars (set X) δ"
by force
then obtain s where s: "s ∈ trms⇩s⇩t⇩p (Inequality X F)" "t = s ⋅ rm_vars (set X) δ" by atomize_elim auto
hence "s ∈ SMP (trms⇩s⇩t S)" using **(1) by force
hence "t ∈ SMP (trms⇩s⇩t 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: "⋃(trms⇩s⇩t⇩p ` set S) ⊆ SMP (trms⇩s⇩t S)" "trms⇩s⇩t S ⊆ SMP (trms⇩s⇩t S)" "M ⊆ SMP M"
by auto
lemma SMP_fun_map_snd_subset: "SMP (trms⇩s⇩t (map Send1 X)) ⊆ SMP (trms⇩s⇩t [Send1 (Fun f X)])"
proof
fix t assume "t ∈ SMP (trms⇩s⇩t (map Send1 X))" thus "t ∈ SMP (trms⇩s⇩t [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" "trms⇩s⇩t [Send1 (Fun f X)]" t] using SMP.MP by auto
qed blast+
qed
lemma SMP_wt_subst_subset:
assumes "t ∈ SMP (M ⋅⇩s⇩e⇩t ℐ)" "wt⇩s⇩u⇩b⇩s⇩t ℐ" "wf⇩t⇩r⇩m⇩s (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 ⋅ δ ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (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 ⋅ δ" "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using assms(1) by fast
have "t ∈ SMP (N ⋅⇩s⇩e⇩t δ)" using n(1,2) SMP_singleton_ex(2)[of m "N ⋅⇩s⇩e⇩t δ", 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 (subterms⇩s⇩e⇩t M) = SMP M"
proof
show "SMP M ⊆ SMP (subterms⇩s⇩e⇩t M)" using SMP_mono[of M "subterms⇩s⇩e⇩t M"] by blast
show "SMP (subterms⇩s⇩e⇩t M) ⊆ SMP M"
proof
fix t show "t ∈ SMP (subterms⇩s⇩e⇩t 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: "wf⇩t⇩r⇩m⇩s 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 ∈ fv⇩s⇩e⇩t 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 tfr⇩s⇩t⇩p (x#S) ⟹ list_all tfr⇩s⇩t⇩p [x]"
"list_all tfr⇩s⇩t⇩p (x#S) ⟹ list_all tfr⇩s⇩t⇩p S"
"list_all tfr⇩s⇩t⇩p (S@S') ⟹ list_all tfr⇩s⇩t⇩p S"
"list_all tfr⇩s⇩t⇩p (S@S') ⟹ list_all tfr⇩s⇩t⇩p S'"
"list_all tfr⇩s⇩t⇩p (S@x#S') ⟹ list_all tfr⇩s⇩t⇩p (S@S')"
by fastforce+
lemma tfr_stp_all_append:
assumes "list_all tfr⇩s⇩t⇩p S" "list_all tfr⇩s⇩t⇩p S'"
shows "list_all tfr⇩s⇩t⇩p (S@S')"
using assms by fastforce
lemma tfr_stp_all_wt_subst_apply:
assumes "list_all tfr⇩s⇩t⇩p S"
and θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
"bvars⇩s⇩t S ∩ range_vars θ = {}"
shows "list_all tfr⇩s⇩t⇩p (S ⋅⇩s⇩t θ)"
using assms(1,4)
proof (induction S)
case (Cons x S)
hence IH: "list_all tfr⇩s⇩t⇩p (S ⋅⇩s⇩t θ)"
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) ⋅⇩s⇩t θ = Equality a (t ⋅ θ) (t' ⋅ θ)#(S ⋅⇩s⇩t θ)"
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 ⋅⇩p⇩a⇩i⇩r⇩s ?σ"
let ?P = "λF X. ∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X. ∃a. Γ (Var x) = TAtom a"
let ?Q = "λF X.
∀f T. Fun f T ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s 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: "fv⇩s⇩e⇩t (?σ ` 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. wf⇩t⇩r⇩m (?σ 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 "∀x∈fv⇩p⇩a⇩i⇩r⇩s (G ⋅⇩p⇩a⇩i⇩r⇩s ?σ) - 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 "trms⇩p⇩a⇩i⇩r⇩s F"] trms⇩p⇩a⇩i⇩r⇩s_subst[of F ?σ]
by presburger
moreover have "(x#S) ⋅⇩s⇩t θ = Inequality X (F ⋅⇩p⇩a⇩i⇩r⇩s ?σ)#(S ⋅⇩s⇩t θ)"
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 tfr⇩s⇩t⇩p (S@Equality a t t'#S') ⟹ Unifier δ t t' ⟹ Γ t = Γ t'"
by force+
lemma tfr_subset:
"⋀A B. tfr⇩s⇩e⇩t (A ∪ B) ⟹ tfr⇩s⇩e⇩t A"
"⋀A B. tfr⇩s⇩e⇩t B ⟹ A ⊆ B ⟹ tfr⇩s⇩e⇩t A"
"⋀A B. tfr⇩s⇩e⇩t B ⟹ SMP A ⊆ SMP B ⟹ tfr⇩s⇩e⇩t A"
proof -
show 1: "tfr⇩s⇩e⇩t (A ∪ B) ⟹ tfr⇩s⇩e⇩t A" for A B
using SMP_union[of A B] unfolding tfr⇩s⇩e⇩t_def by simp
fix A B assume B: "tfr⇩s⇩e⇩t B"
show "A ⊆ B ⟹ tfr⇩s⇩e⇩t 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 ⟹ tfr⇩s⇩e⇩t 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 tfr⇩s⇩e⇩t_def by blast
qed
qed
lemma tfr_empty[simp]: "tfr⇩s⇩e⇩t {}"
unfolding tfr⇩s⇩e⇩t_def by simp
lemma tfr_consts_mono:
assumes "∀t ∈ M. ∃c. t = Fun c []"
and "∀t ∈ M. Ana t = ([], [])"
and "tfr⇩s⇩e⇩t N"
shows "tfr⇩s⇩e⇩t (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 tfr⇩s⇩e⇩t_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 tfr⇩s⇩e⇩t_def)
qed
lemma dual⇩s⇩t_tfr⇩s⇩t⇩p: "list_all tfr⇩s⇩t⇩p S ⟹ list_all tfr⇩s⇩t⇩p (dual⇩s⇩t S)"
proof (induction S)
case (Cons x S)
have "list_all tfr⇩s⇩t⇩p S" using Cons.prems by simp
hence IH: "list_all tfr⇩s⇩t⇩p (dual⇩s⇩t 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 (dual⇩s⇩t (x#S)) = insert x (set (dual⇩s⇩t S))" using Inequality by auto
moreover have "(∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X. ∃a. Γ (Var x) = Var a) ∨
(∀f T. Fun f T ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s 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 "wt⇩s⇩u⇩b⇩s⇩t δ"
shows "wt⇩s⇩u⇩b⇩s⇩t (subst_var_inv δ X)"
using assms f_inv_into_f[of _ δ X]
unfolding wt⇩s⇩u⇩b⇩s⇩t_def subst_var_inv_def
by presburger
lemma subst_var_inv_wf_trms:
"wf⇩t⇩r⇩m⇩s (subst_range (subst_var_inv δ X))"
using f_inv_into_f[of _ δ X]
unfolding wt⇩s⇩u⇩b⇩s⇩t_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. wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m 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 "wf⇩t⇩r⇩m (Fun f X)" "wf⇩t⇩r⇩m (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'. wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m 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 "wf⇩t⇩r⇩m s" "wf⇩t⇩r⇩m t"
using wf_trm_subterm ‹wf⇩t⇩r⇩m (Fun f X)› ‹wf⇩t⇩r⇩m (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 ‹wf⇩t⇩r⇩m (Fun f X)› * ‹(s,t) ∈ set E'› unfolding wf⇩t⇩r⇩m_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 "wf⇩t⇩r⇩m s" "wf⇩t⇩r⇩m t" "Γ s = Γ t" by metis+
}
thus ?thesis by blast
qed
moreover have "∀(s,t) ∈ set E. wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m 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" "wf⇩t⇩r⇩m t" by auto
hence "wt⇩s⇩u⇩b⇩s⇩t (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 wt⇩s⇩u⇩b⇩s⇩t_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). wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m t"
using wf_trm_subst_singleton[OF _ ‹wf⇩t⇩r⇩m 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 ‹wt⇩s⇩u⇩b⇩s⇩t (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)" "wf⇩t⇩r⇩m (Fun f X)" by auto
hence "wt⇩s⇩u⇩b⇩s⇩t (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 wt⇩s⇩u⇩b⇩s⇩t_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). wf⇩t⇩r⇩m s ∧ wf⇩t⇩r⇩m t"
using wf_trm_subst_singleton[OF _ ‹wf⇩t⇩r⇩m (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 ‹wt⇩s⇩u⇩b⇩s⇩t (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 σ" "wf⇩t⇩r⇩m s" "wf⇩t⇩r⇩m t" "Γ s = Γ t"
shows "wt⇩s⇩u⇩b⇩s⇩t σ"
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 "wt⇩s⇩u⇩b⇩s⇩t σ" using ‹subst_of σ' = σ› unfolding wt⇩s⇩u⇩b⇩s⇩t_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: "wf⇩t⇩r⇩m s" "wf⇩t⇩r⇩m t" "Γ s = Γ t"
and δ: "Unifier δ s t"
shows "∃θ. Unifier θ s t ∧ wt⇩s⇩u⇩b⇩s⇩t θ ∧ wf⇩t⇩r⇩m⇩s (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 ∈ fv⇩s⇩e⇩t 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) ∧
wf⇩t⇩r⇩m⇩s' arity M ∧
has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M ∧
has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M ∧
is_TComp_var_instance_closed Γ M"
definition comp_tfr⇩s⇩e⇩t where
"comp_tfr⇩s⇩e⇩t arity Ana Γ M ≡
finite_SMP_representation arity Ana Γ M ∧
(let δ = var_rename (max_var_set (fv⇩s⇩e⇩t M))
in ∀s ∈ M. ∀t ∈ M. is_Fun s ∧ is_Fun t ∧ Γ s ≠ Γ t ⟶ mgu s (t ⋅ δ) = None)"
fun comp_tfr⇩s⇩t⇩p where
"comp_tfr⇩s⇩t⇩p Γ (⟨_: t ≐ t'⟩⇩s⇩t) = (mgu t t' ≠ None ⟶ Γ t = Γ t')"
| "comp_tfr⇩s⇩t⇩p Γ (∀X⟨∨≠: F⟩⇩s⇩t) = (
(∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X. is_Var (Γ (Var x))) ∨
(∀u ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F).
is_Fun u ⟶ (args u = [] ∨ (∃s ∈ set (args u). s ∉ Var ` set X))))"
| "comp_tfr⇩s⇩t⇩p _ _ = True"
definition comp_tfr⇩s⇩t where
"comp_tfr⇩s⇩t arity Ana Γ M S ≡
list_all (comp_tfr⇩s⇩t⇩p Γ) S ∧
list_all (wf⇩t⇩r⇩m' arity) (trms_list⇩s⇩t S) ∧
has_all_wt_instances_of Γ (trms⇩s⇩t S) M ∧
comp_tfr⇩s⇩e⇩t 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 "wf⇩t⇩r⇩m⇩s M"
and "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t 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 wf⇩t⇩r⇩m⇩s_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: "wf⇩t⇩r⇩m t"
and s_wf_trm: "wf⇩t⇩r⇩m s"
and t_instance_s: "is_wt_instance_of_cond Γ t s"
shows "∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (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: "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m 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: "wf⇩t⇩r⇩m 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 δ: "wt⇩s⇩u⇩b⇩s⇩t δ" 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: "wf⇩t⇩r⇩m⇩s N"
and M_wf_trms: "wf⇩t⇩r⇩m⇩s M"
and N_instance_M: "has_all_wt_instances_of Γ N M"
and t_in_N: "t ∈ N"
shows "∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t ∈ M ⋅⇩s⇩e⇩t δ"
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: "wf⇩t⇩r⇩m⇩s N"
and M_wf_trms: "wf⇩t⇩r⇩m⇩s 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: "wf⇩t⇩r⇩m⇩s N"
and M_wf_trms: "wf⇩t⇩r⇩m⇩s 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 ⋅⇩l⇩i⇩s⇩t δ,R ⋅⇩l⇩i⇩s⇩t δ)) ∨
(∀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 (fv⇩s⇩e⇩t M))) = {}"
proof -
have 1: "∀v ∈ fv s. snd v ≤ max_var_set (fv⇩s⇩e⇩t M)" using assms
proof (induction M rule: finite_induct)
case (insert t M) thus ?case
proof (cases "t = s")
case False
hence "∀v ∈ fv s. snd v ≤ max_var_set (fv⇩s⇩e⇩t M)" using insert by simp
moreover have "max_var_set (fv⇩s⇩e⇩t M) ≤ max_var_set (fv⇩s⇩e⇩t (insert t M))"
using insert.hyps(1) insert.prems
by force
ultimately show ?thesis by auto
qed simp
qed 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"
shows "fv⇩s⇩e⇩t M ∩ fv⇩s⇩e⇩t (N ⋅⇩s⇩e⇩t var_rename (max_var_set (fv⇩s⇩e⇩t M))) = {}"
using var_rename_fv_set_disjoint[OF assms] by auto
lemma var_rename_is_renaming[simp]:
"subst_range (var_rename n) ⊆ range Var"
"subst_range (var_rename_inv n) ⊆ range Var"
unfolding var_rename_def var_rename_inv_def by auto
lemma var_rename_wt[simp]:
"wt⇩s⇩u⇩b⇩s⇩t (var_rename n)"
"wt⇩s⇩u⇩b⇩s⇩t (var_rename_inv n)"
by (auto simp add: var_rename_def var_rename_inv_def wt⇩s⇩u⇩b⇩s⇩t_def Γ_Var_fst)
lemma var_rename_wt':
assumes "wt⇩s⇩u⇩b⇩s⇩t δ" "s = m ⋅ δ"
shows "wt⇩s⇩u⇩b⇩s⇩t (var_rename_inv n ∘⇩s δ)" "s = m ⋅ var_rename n ⋅ var_rename_inv n ∘⇩s δ"
using assms(2) wt_subst_compose[OF var_rename_wt(2)[of n] assms(1)] var_rename_inv_comp[of m n]
by force+
lemma var_rename_wf⇩t⇩r⇩m⇩s_range[simp]:
"wf⇩t⇩r⇩m⇩s (subst_range (var_rename n))"
"wf⇩t⇩r⇩m⇩s (subst_range (var_rename_inv n))"
using var_rename_is_renaming by fastforce+
lemma Fun_range_case:
"(∀f T. Fun f T ∈ M ⟶ P f T) ⟷ (∀u ∈ M. case u of Fun f T ⇒ P f T | _ ⇒ True)"
"(∀f T. Fun f T ∈ M ⟶ P f T) ⟷ (∀u ∈ M. is_Fun u ⟶ P (the_Fun u) (args u))"
by (auto split: "term.splits")
lemma is_TComp_var_instance_closedD:
assumes x: "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var x) = Γ (Var y)" "Γ (Var x) = TComp f T"
and closed: "is_TComp_var_instance_closed Γ M"
shows "∃g U. Fun g U ∈ M ∧ Γ (Fun g U) = Γ (Var x) ∧ (∀u ∈ set U. is_Var u) ∧ distinct U"
using assms unfolding is_TComp_var_instance_closed_def list_all_iff list_ex_iff by fastforce
lemma is_TComp_var_instance_closedD':
assumes "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var x) = Γ (Var y)" "TComp f T ⊑ Γ (Var x)"
and closed: "is_TComp_var_instance_closed Γ M"
and wf: "wf⇩t⇩r⇩m⇩s M"
shows "∃g U. Fun g U ∈ M ∧ Γ (Fun g U) = TComp f T ∧ (∀u ∈ set U. is_Var u) ∧ distinct U"
using assms(1,2)
proof (induction "Γ (Var x)" arbitrary: x)
case (Fun g U)
note IH = Fun.hyps(1)
have g: "arity g > 0" using Fun.hyps(2) fun_type_inv[of "Var x"] Γ_Var_fst by simp_all
then obtain V where V:
"Fun g V ∈ M" "Γ (Fun g V) = Γ (Var x)" "∀v ∈ set V. ∃x. v = Var x"
"distinct V" "length U = length V"
using is_TComp_var_instance_closedD[OF Fun.prems(1) Fun.hyps(2)[symmetric] closed(1)]
by (metis Fun.hyps(2) fun_type_id_eq fun_type_length_eq is_VarE)
hence U: "U = map Γ V" using fun_type[OF g(1), of V] Fun.hyps(2) by simp
hence 1: "Γ v ∈ set U" when v: "v ∈ set V" for v using v by simp
have 2: "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var z) = Γ (Var y)" when z: "Var z ∈ set V" for z
using V(1) fv_subset_subterms Fun_param_in_subterms[OF z] by fastforce
show ?case
proof (cases "TComp f T = Γ (Var x)")
case False
then obtain u where u: "u ∈ set U" "TComp f T ⊑ u"
using Fun.prems(2) Fun.hyps(2) by atomize_elim auto
then obtain y where y: "Var y ∈ set V" "Γ (Var y) = u" using U V(3) Γ_Var_fst by auto
show ?thesis using IH[OF _ 2[OF y(1)]] u y(2) by metis
qed (use V in fastforce)
qed simp
lemma TComp_var_instance_wt_subst_exists:
assumes gT: "Γ (Fun g T) = TComp g (map Γ U)" "wf⇩t⇩r⇩m (Fun g T)"
and U: "∀u ∈ set U. ∃y. u = Var y" "distinct U"
shows "∃θ. wt⇩s⇩u⇩b⇩s⇩t θ ∧ wf⇩t⇩r⇩m⇩s (subst_range θ) ∧ Fun g T = Fun g U ⋅ θ"
proof -
define the_i where "the_i ≡ λy. THE x. x < length U ∧ U ! x = Var y"
define θ where θ: "θ ≡ λy. if Var y ∈ set U then T ! the_i y else Var y"
have g: "arity g > 0" using gT(1,2) fun_type_inv(1) by blast
have UT: "length U = length T" using fun_type_length_eq gT(1) by fastforce
have 1: "the_i y < length U ∧ U ! the_i y = Var y" when y: "Var y ∈ set U" for y
using theI'[OF distinct_Ex1[OF U(2) y]] unfolding the_i_def by simp
have 2: "wt⇩s⇩u⇩b⇩s⇩t θ"
using θ 1 gT(1) fun_type[OF g] UT
unfolding wt⇩s⇩u⇩b⇩s⇩t_def
by (metis (no_types, lifting) nth_map term.inject(2))
have "∀i<length T. U ! i ⋅ θ = T ! i"
using θ 1 U(1) UT distinct_Ex1[OF U(2)] in_set_conv_nth
by (metis (no_types, lifting) eval_term.simps(1))
hence "T = map (λt. t ⋅ θ) U" by (simp add: UT nth_equalityI)
hence 3: "Fun g T = Fun g U ⋅ θ" by simp
have "subst_range θ ⊆ set T" using θ 1 U(1) UT by (auto simp add: subst_domain_def)
hence 4: "wf⇩t⇩r⇩m⇩s (subst_range θ)" using gT(2) wf_trm_param by auto
show ?thesis by (metis 2 3 4)
qed
lemma TComp_var_instance_closed_has_Var:
assumes closed: "is_TComp_var_instance_closed Γ M"
and wf_M: "wf⇩t⇩r⇩m⇩s M"
and wf_δx: "wf⇩t⇩r⇩m (δ x)"
and y_ex: "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var x) = Γ (Var y)"
and t: "t ⊑ δ x"
and δ_wt: "wt⇩s⇩u⇩b⇩s⇩t δ"
shows "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var y) = Γ t"
proof (cases "Γ (Var x)")
case (Var a)
hence "t = δ x"
using t wf_δx δ_wt
by (metis (full_types) const_type_inv_wf fun_if_subterm subtermeq_Var_const(2) wt⇩s⇩u⇩b⇩s⇩t_def)
thus ?thesis using y_ex wt_subst_trm''[OF δ_wt, of "Var x"] by fastforce
next
case (Fun f T)
hence Γ_δx: "Γ (δ x) = TComp f T" using wt_subst_trm''[OF δ_wt, of "Var x"] by auto
show ?thesis
proof (cases "t = δ x")
case False
hence t_subt_δx: "t ⊏ δ x" using t(1) Γ_δx by fastforce
obtain T' where T': "δ x = Fun f T'" using Γ_δx t_subt_δx fun_type_id_eq by (cases "δ x") auto
obtain g S where gS: "Fun g S ⊑ δ x" "t ∈ set S" using Fun_ex_if_subterm[OF t_subt_δx] by blast
have gS_wf: "wf⇩t⇩r⇩m (Fun g S)" by (rule wf_trm_subtermeq[OF wf_δx gS(1)])
hence "arity g > 0" using gS(2) by (metis length_pos_if_in_set wf_trm_arity)
hence gS_Γ: "Γ (Fun g S) = TComp g (map Γ S)" using fun_type by blast
obtain h U where hU:
"Fun h U ∈ M" "Γ (Fun h U) = Fun g (map Γ S)" "∀u ∈ set U. is_Var u"
using is_TComp_var_instance_closedD'[OF y_ex _ closed wf_M]
subtermeq_imp_subtermtypeeq[OF wf_δx] gS Γ_δx Fun gS_Γ
by metis
obtain y where y: "Var y ∈ set U" "Γ (Var y) = Γ t"
using hU(3) fun_type_param_ex[OF hU(2) gS(2)] by fast
have "y ∈ fv⇩s⇩e⇩t M" using hU(1) y(1) by force
thus ?thesis using y(2) closed by metis
qed (metis y_ex Fun Γ_δx)
qed
lemma TComp_var_instance_closed_has_Fun:
assumes closed: "is_TComp_var_instance_closed Γ M"
and wf_M: "wf⇩t⇩r⇩m⇩s M"
and wf_δx: "wf⇩t⇩r⇩m (δ x)"
and y_ex: "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var x) = Γ (Var y)"
and t: "t ⊑ δ x"
and δ_wt: "wt⇩s⇩u⇩b⇩s⇩t δ"
and t_Γ: "Γ t = TComp g T"
and t_fun: "is_Fun t"
shows "∃m ∈ M. ∃θ. wt⇩s⇩u⇩b⇩s⇩t θ ∧ wf⇩t⇩r⇩m⇩s (subst_range θ) ∧ t = m ⋅ θ ∧ is_Fun m"
proof -
obtain T'' where T'': "t = Fun g T''" using t_Γ t_fun fun_type_id_eq by blast
have g: "arity g > 0" using t_Γ fun_type_inv[of t] by simp_all
have "TComp g T ⊑ Γ (Var x)" using δ_wt t t_Γ
by (metis wf_δx subtermeq_imp_subtermtypeeq wt⇩s⇩u⇩b⇩s⇩t_def)
then obtain U where U:
"Fun g U ∈ M" "Γ (Fun g U) = TComp g T" "∀u ∈ set U. ∃y. u = Var y"
"distinct U" "length T'' = length U"
using is_TComp_var_instance_closedD'[OF y_ex _ closed wf_M]
by (metis t_Γ T'' fun_type_id_eq fun_type_length_eq is_VarE)
hence UT': "T = map Γ U" using fun_type[OF g, of U] by simp
show ?thesis
using TComp_var_instance_wt_subst_exists UT' T'' U(1,3,4) t t_Γ wf_δx wf_trm_subtermeq
by (metis term.disc(2))
qed
lemma TComp_var_and_subterm_instance_closed_has_subterms_instances:
assumes M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
and M_subterms_cl: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
and M_wf: "wf⇩t⇩r⇩m⇩s M"
and t: "t ⊑⇩s⇩e⇩t M"
and s: "s ⊑ t ⋅ δ"
and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "∃m ∈ M. ∃θ. wt⇩s⇩u⇩b⇩s⇩t θ ∧ wf⇩t⇩r⇩m⇩s (subst_range θ) ∧ s = m ⋅ θ"
using subterm_subst_unfold[OF s]
proof
assume "∃s'. s' ⊑ t ∧ s = s' ⋅ δ"
then obtain s' where s': "s' ⊑ t" "s = s' ⋅ δ" by blast
then obtain θ where θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "s' ∈ M ⋅⇩s⇩e⇩t θ"
using t has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
term.order_trans[of s' t]
by blast
then obtain m where m: "m ∈ M" "s' = m ⋅ θ" by blast
have "s = m ⋅ (θ ∘⇩s δ)" using s'(2) m(2) by simp
thus ?thesis
using m(1) wt_subst_compose[OF θ(1) δ(1)] wf_trms_subst_compose[OF θ(2) δ(2)] by blast
next
assume "∃x ∈ fv t. s ⊏ δ x"
then obtain x where x: "x ∈ fv t" "s ⊏ δ x" "s ⊑ δ x" by blast
note 0 = TComp_var_instance_closed_has_Var[OF M_var_inst_cl M_wf]
note 1 = has_all_wt_instances_ofD''[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
have δx_wf: "wf⇩t⇩r⇩m (δ x)" and s_wf_trm: "wf⇩t⇩r⇩m s"
using δ(2) wf_trm_subterm[OF _ x(2)] by fastforce+
have x_fv_ex: "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var x) = Γ (Var y)"
using x(1) s fv_subset_subterms[OF t] by auto
obtain y where y: "y ∈ fv⇩s⇩e⇩t M" "Γ (Var y) = Γ s"
using 0[of δ x s, OF δx_wf x_fv_ex x(3) δ(1)] by metis
then obtain z where z: "Var z ∈ M" "Γ (Var z) = Γ s"
using 1[of y] vars_iff_subtermeq_set[of y M] by metis
define θ where "θ ≡ Var(z := s)::('fun, ('fun, 'atom) term × nat) subst"
have "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "s = Var z ⋅ θ"
using z(2) s_wf_trm unfolding θ_def wt⇩s⇩u⇩b⇩s⇩t_def by force+
thus ?thesis using z(1) by blast
qed
context
begin
private lemma SMP_D_aux1:
assumes "t ∈ SMP M"
and closed: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
"is_TComp_var_instance_closed Γ M"
and wf_M: "wf⇩t⇩r⇩m⇩s M"
shows "∀x ∈ fv t. ∃y ∈ fv⇩s⇩e⇩t M. Γ (Var y) = Γ (Var x)"
using assms(1)
proof (induction t rule: SMP.induct)
case (MP t) show ?case
proof
fix x assume x: "x ∈ fv t"
hence "Var x ∈ subterms⇩s⇩e⇩t M" using MP.hyps vars_iff_subtermeq by fastforce
then obtain δ s where δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
and s: "s ∈ M" "Var x = s ⋅ δ"
using has_all_wt_instances_ofD'[OF wf_trms_subterms[OF wf_M] wf_M closed(1)] by blast
then obtain y where y: "s = Var y" by (cases s) auto
thus "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var y) = Γ (Var x)"
using s wt_subst_trm''[OF δ(1), of "Var y"] by force
qed
next
case (Subterm t t')
hence "fv t' ⊆ fv t" using subtermeq_vars_subset by auto
thus ?case using Subterm.IH by auto
next
case (Substitution t δ)
note IH = Substitution.IH
show ?case
proof
fix x assume x: "x ∈ fv (t ⋅ δ)"
then obtain y where y: "y ∈ fv t" "Γ (Var x) ⊑ Γ (Var y)"
using Substitution.hyps(2,3)
by (metis subst_apply_img_var subtermeqI' subtermeq_imp_subtermtypeeq
vars_iff_subtermeq wt⇩s⇩u⇩b⇩s⇩t_def wf_trm_subst_rangeD)
let ?P = "λx. ∃y ∈ fv⇩s⇩e⇩t M. Γ (Var y) = Γ (Var x)"
show "?P x" using y IH
proof (induction "Γ (Var y)" arbitrary: y t)
case (Var a)
hence "Γ (Var x) = Γ (Var y)" by auto
thus ?case using Var(2,4) by auto
next
case (Fun f T)
obtain z where z: "∃w ∈ fv⇩s⇩e⇩t M. Γ (Var z) = Γ (Var w)" "Γ (Var z) = Γ (Var y)"
using Fun.prems(1,3) by blast
show ?case
proof (cases "Γ (Var x) = Γ (Var y)")
case True thus ?thesis using Fun.prems by auto
next
case False
then obtain τ where τ: "τ ∈ set T" "Γ (Var x) ⊑ τ" using Fun.prems(2) Fun.hyps(2) by auto
then obtain U where U:
"Fun f U ∈ M" "Γ (Fun f U) = Γ (Var z)" "∀u ∈ set U. ∃v. u = Var v" "distinct U"
using is_TComp_var_instance_closedD'[OF z(1) _ closed(2) wf_M] Fun.hyps(2) z(2)
by (metis fun_type_id_eq subtermeqI' is_VarE)
hence 1: "∀x ∈ fv (Fun f U). ∃y ∈ fv⇩s⇩e⇩t M. Γ (Var y) = Γ (Var x)" by force
have "arity f > 0" using U(2) z(2) Fun.hyps(2) fun_type_inv(1) by metis
hence "Γ (Fun f U) = TComp f (map Γ U)" using fun_type by auto
then obtain u where u: "Var u ∈ set U" "Γ (Var u) = τ"
using τ(1) U(2,3) z(2) Fun.hyps(2) by auto
show ?thesis
using Fun.hyps(1)[of u "Fun f U"] u τ 1
by force
qed
qed
qed
next
case (Ana t K T k)
have "fv k ⊆ fv t" using Ana_keys_fv[OF Ana.hyps(2)] Ana.hyps(3) by auto
thus ?case using Ana.IH by auto
qed
private lemma SMP_D_aux2:
fixes t::"('fun, ('fun, 'atom) term × nat) term"
assumes t_SMP: "t ∈ SMP M"
and t_Var: "∃x. t = Var x"
and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
shows "∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = m ⋅ δ"
proof -
have M_wf: "wf⇩t⇩r⇩m⇩s M"
and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
and M_subterms_cl: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
using finite_SMP_representationD[OF M_SMP_repr] by blast+
have M_Ana_wf: "wf⇩t⇩r⇩m⇩s (⋃ ((set ∘ fst ∘ Ana) ` M))"
proof
fix k assume "k ∈ ⋃((set ∘ fst ∘ Ana) ` M)"
then obtain m where m: "m ∈ M" "k ∈ set (fst (Ana m))" by force
thus "wf⇩t⇩r⇩m k" using M_wf Ana_keys_wf'[of m "fst (Ana m)" _ k] surjective_pairing by blast
qed
note 0 = has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
note 1 = has_all_wt_instances_ofD'[OF M_Ana_wf M_wf M_Ana_cl]
obtain x y where x: "t = Var x" and y: "y ∈ fv⇩s⇩e⇩t M" "Γ (Var y) = Γ (Var x)"
using t_Var SMP_D_aux1[OF t_SMP M_subterms_cl M_var_inst_cl M_wf] by fastforce
then obtain m δ where m: "m ∈ M" "m ⋅ δ = Var y" and δ: "wt⇩s⇩u⇩b⇩s⇩t δ"
using 0[of "Var y"] vars_iff_subtermeq_set[of y M] by fastforce
obtain z where z: "m = Var z" using m(2) by (cases m) auto
define θ where "θ ≡ Var(z := Var x)::('fun, ('fun, 'atom) term × nat) subst"
have "Γ (Var z) = Γ (Var x)" using y(2) m(2) z wt_subst_trm''[OF δ, of m] by argo
hence "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" unfolding θ_def wt⇩s⇩u⇩b⇩s⇩t_def by force+
moreover have "t = m ⋅ θ" using x z unfolding θ_def by simp
ultimately show ?thesis using m(1) by blast
qed
private lemma SMP_D_aux3:
assumes hyps: "t' ⊑ t" and wf_t: "wf⇩t⇩r⇩m t" and prems: "is_Fun t'"
and IH:
"((∃f. t = Fun f []) ∧ (∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = m ⋅ δ)) ∨
(∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = m ⋅ δ ∧ is_Fun m)"
and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
shows "((∃f. t' = Fun f []) ∧ (∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t' = m ⋅ δ)) ∨
(∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t' = m ⋅ δ ∧ is_Fun m)"
proof (cases "∃f. t = Fun f [] ∨ t' = Fun f []")
case True
have M_wf: "wf⇩t⇩r⇩m⇩s M"
and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
and M_subterms_cl: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
using finite_SMP_representationD[OF M_SMP_repr] by blast+
note 0 = has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
note 1 = TComp_var_instance_closed_has_Fun[OF M_var_inst_cl M_wf]
note 2 = TComp_var_and_subterm_instance_closed_has_subterms_instances[
OF M_var_inst_cl M_subterms_cl M_wf]
have wf_t': "wf⇩t⇩r⇩m t'" using hyps wf_t wf_trm_subterm by blast
obtain c where "t = Fun c [] ∨ t' = Fun c []" using True by atomize_elim auto
thus ?thesis
proof
assume c: "t' = Fun c []"
show ?thesis
proof (cases "∃f. t = Fun f []")
case True
hence "t = t'" using c hyps by force
thus ?thesis using IH by fast
next
case False
note F = this
then obtain m δ where m: "m ∈ M" "t = m ⋅ δ"
and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using IH by blast
show ?thesis using subterm_subst_unfold[OF hyps[unfolded m(2)]]
proof
assume "∃m'. m' ⊑ m ∧ t' = m' ⋅ δ"
then obtain m' where m': "m' ⊑ m" "t' = m' ⋅ δ" by atomize_elim auto
obtain n θ where n: "n ∈ M" "m' = n ⋅ θ" and θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
using 0[of m'] m(1) m'(1) by blast
have "t' = n ⋅ (θ ∘⇩s δ)" using m'(2) n(2) by auto
thus ?thesis
using c n(1) wt_subst_compose[OF θ(1) δ(1)] wf_trms_subst_compose[OF θ(2) δ(2)] by blast
next
assume "∃x ∈ fv m. t' ⊏ δ x"
then obtain x where x: "x ∈ fv m" "t' ⊏ δ x" "t' ⊑ δ x" by atomize_elim auto
have δx_wf: "wf⇩t⇩r⇩m (δ x)" using δ(2) by fastforce
have x_fv_ex: "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var x) = Γ (Var y)" using x m by auto
show ?thesis
proof (cases "Γ t'")
case (Var a)
show ?thesis
using c m 2[OF _ hyps[unfolded m(2)] δ]
by fast
next
case (Fun g S)
show ?thesis
using c 1[of δ x t', OF δx_wf x_fv_ex x(3) δ(1) Fun]
by blast
qed
qed
qed
qed (use IH hyps in simp)
next
case False
note F = False
then obtain m δ where m:
"m ∈ M" "wt⇩s⇩u⇩b⇩s⇩t δ" "t = m ⋅ δ" "is_Fun m" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using IH by atomize_elim auto
obtain f T where fT: "t' = Fun f T" "arity f > 0" "Γ t' = TComp f (map Γ T)"
using F prems fun_type wf_trm_subtermeq[OF wf_t hyps]
by (metis is_FunE length_greater_0_conv subtermeqI' wf⇩t⇩r⇩m_def)
have closed: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
"is_TComp_var_instance_closed Γ M"
using M_SMP_repr unfolding finite_SMP_representation_def by metis+
have M_wf: "wf⇩t⇩r⇩m⇩s M"
using finite_SMP_representationD[OF M_SMP_repr] by blast
show ?thesis
proof (cases "∃x ∈ fv m. t' ⊑ δ x")
case True
then obtain x where x: "x ∈ fv m" "t' ⊑ δ x" by atomize_elim auto
have 1: "x ∈ fv⇩s⇩e⇩t M" using m(1) x(1) by auto
have 2: "is_Fun (δ x)" using prems x(2) by auto
have 3: "wf⇩t⇩r⇩m (δ x)" using m(5) by (simp add: wf_trm_subst_rangeD)
have "¬(∃f. δ x = Fun f [])" using F x(2) by auto
hence "∃f T. Γ (Var x) = TComp f T" using 2 3 m(2)
by (metis (no_types) fun_type is_FunE length_greater_0_conv subtermeqI' wf⇩t⇩r⇩m_def wt⇩s⇩u⇩b⇩s⇩t_def)
moreover have "∃f T. Γ t' = Fun f T"
using False prems wf_trm_subtermeq[OF wf_t hyps]
by (metis (no_types) fun_type is_FunE length_greater_0_conv subtermeqI' wf⇩t⇩r⇩m_def)
ultimately show ?thesis
using TComp_var_instance_closed_has_Fun 1 x(2) m(2) prems closed 3 M_wf
by metis
next
case False
then obtain m' where m': "m' ⊑ m" "t' = m' ⋅ δ" "is_Fun m'"
using hyps m(3) subterm_subst_not_img_subterm
by blast
then obtain θ m'' where θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "m'' ∈ M" "m' = m'' ⋅ θ"
using m(1) has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf closed(1)] by blast
hence t'_m'': "t' = m'' ⋅ θ ∘⇩s δ" using m'(2) by fastforce
note θδ = wt_subst_compose[OF θ(1) m(2)] wf_trms_subst_compose[OF θ(2) m(5)]
show ?thesis
proof (cases "is_Fun m''")
case True thus ?thesis using θ(3,4) m'(2,3) m(4) fT t'_m'' θδ by blast
next
case False
then obtain x where x: "m'' = Var x" by atomize_elim auto
hence "∃y ∈ fv⇩s⇩e⇩t M. Γ (Var x) = Γ (Var y)" "t' ⊑ (θ ∘⇩s δ) x"
"Γ (Var x) = Fun f (map Γ T)" "wf⇩t⇩r⇩m ((θ ∘⇩s δ) x)"
using θδ t'_m'' θ(3) fv_subset[OF θ(3)] fT(3) eval_term.simps(1)[of _ "θ ∘⇩s δ"]
wt_subst_trm''[OF θδ(1), of "Var x"]
by force+
thus ?thesis
using x TComp_var_instance_closed_has_Fun[
of M "θ ∘⇩s δ" x t' f "map Γ T", OF closed(2) M_wf _ _ _ θδ(1) fT(3) prems]
by blast
qed
qed
qed
lemma SMP_D:
assumes "t ∈ SMP M" "is_Fun t"
and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
shows "((∃f. t = Fun f []) ∧ (∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = m ⋅ δ)) ∨
(∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = m ⋅ δ ∧ is_Fun m)"
proof -
have wf_M: "wf⇩t⇩r⇩m⇩s M"
and closed: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
"has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
"is_TComp_var_instance_closed Γ M"
using finite_SMP_representationD[OF M_SMP_repr] by blast+
show ?thesis using assms(1,2)
proof (induction t rule: SMP.induct)
case (MP t)
moreover have "wt⇩s⇩u⇩b⇩s⇩t Var" "wf⇩t⇩r⇩m⇩s (subst_range Var)" "t = t ⋅ Var" by simp_all
ultimately show ?case by blast
next
case (Subterm t t')
hence t_fun: "is_Fun t" by auto
note * = Subterm.hyps(2) SMP_wf_trm[OF Subterm.hyps(1) wf_M(1)]
Subterm.prems Subterm.IH[OF t_fun] M_SMP_repr
show ?case by (rule SMP_D_aux3[OF *])
next
case (Substitution t δ)
have wf: "wf⇩t⇩r⇩m t" by (metis Substitution.hyps(1) wf_M(1) SMP_wf_trm)
hence wf': "wf⇩t⇩r⇩m (t ⋅ δ)" using Substitution.hyps(3) wf_trm_subst by blast
show ?case
proof (cases "Γ t")
case (Var a)
hence 1: "Γ (t ⋅ δ) = TAtom a" using Substitution.hyps(2) by (metis wt_subst_trm'')
then obtain c where c: "t ⋅ δ = Fun c []"
using TAtom_term_cases[OF wf' 1] Substitution.prems by fastforce
hence "(∃x. t = Var x) ∨ t = t ⋅ δ" by (cases t) auto
thus ?thesis
proof
assume t_Var: "∃x. t = Var x"
then obtain x where x: "t = Var x" "δ x = Fun c []" "Γ (Var x) = TAtom a"
using c 1 wt_subst_trm''[OF Substitution.hyps(2), of t] by force
obtain m θ where m: "m ∈ M" "t = m ⋅ θ" and θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
using SMP_D_aux2[OF Substitution.hyps(1) t_Var M_SMP_repr] by atomize_elim auto
have "m ⋅ (θ ∘⇩s δ) = Fun c []" using c m(2) by auto
thus ?thesis
using c m(1) wt_subst_compose[OF θ(1) Substitution.hyps(2)]
wf_trms_subst_compose[OF θ(2) Substitution.hyps(3)]
by metis
qed (use c Substitution.IH in auto)
next
case (Fun f T)
hence 1: "Γ (t ⋅ δ) = TComp f T" using Substitution.hyps(2) by (metis wt_subst_trm'')
have 2: "¬(∃f. t = Fun f [])" using Fun TComp_term_cases[OF wf] by auto
obtain T'' where T'': "t ⋅ δ = Fun f T''"
using 1 2 fun_type_id_eq Fun Substitution.prems
by fastforce
have f: "arity f > 0" using fun_type_inv[OF 1] by metis
show ?thesis
proof (cases t)
case (Fun g U)
then obtain m θ where m:
"m ∈ M" "wt⇩s⇩u⇩b⇩s⇩t θ" "t = m ⋅ θ" "is_Fun m" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
using Substitution.IH Fun 2 by atomize_elim auto
have "wt⇩s⇩u⇩b⇩s⇩t (θ ∘⇩s δ)" "t ⋅ δ = m ⋅ (θ ∘⇩s δ)" "wf⇩t⇩r⇩m⇩s (subst_range (θ ∘⇩s δ))"
using wt_subst_compose[OF m(2) Substitution.hyps(2)] m(3)
wf_trms_subst_compose[OF m(5) Substitution.hyps(3)]
by auto
thus ?thesis using m(1,4) by metis
next
case (Var x)
then obtain y where y: "y ∈ fv⇩s⇩e⇩t M" "Γ (Var y) = Γ (Var x)"
using SMP_D_aux1[OF Substitution.hyps(1) closed(1,3) wf_M] Fun
by atomize_elim auto
hence 3: "Γ (Var y) = TComp f T" using Var Fun Γ_Var_fst by simp
obtain h V where V:
"Fun h V ∈ M" "Γ (Fun h V) = Γ (Var y)" "∀u ∈ set V. ∃z. u = Var z" "distinct V"
by (metis is_VarE is_TComp_var_instance_closedD[OF _ 3 closed(3)] y(1))
moreover have "length T'' = length V" using 3 V(2) fun_type_length_eq 1 T'' by metis
ultimately have TV: "T = map Γ V"
by (metis fun_type[OF f(1)] 3 fun_type_id_eq term.inject(2))
obtain θ where θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "t ⋅ δ = Fun h V ⋅ θ"
using TComp_var_instance_wt_subst_exists 1 3 T'' TV V(2,3,4) wf'
by (metis fun_type_id_eq)
have 9: "Γ (Fun h V) = Γ (δ x)" using y(2) Substitution.hyps(2) V(2) 1 3 Var by auto
show ?thesis using Var θ 9 V(1) by force
qed
qed
next
case (Ana t K T k)
have 1: "is_Fun t" using Ana.hyps(2,3) by auto
then obtain f U where U: "t = Fun f U" by atomize_elim auto
have 2: "fv k ⊆ fv t" using Ana_keys_fv[OF Ana.hyps(2)] Ana.hyps(3) by auto
have wf_t: "wf⇩t⇩r⇩m t"
using SMP_wf_trm[OF Ana.hyps(1)] wf⇩t⇩r⇩m_code wf_M
by auto
hence wf_k: "wf⇩t⇩r⇩m k"
using Ana_keys_wf'[OF Ana.hyps(2)] wf⇩t⇩r⇩m_code Ana.hyps(3)
by auto
have wf_M_keys: "wf⇩t⇩r⇩m⇩s (⋃((set ∘ fst ∘ Ana) ` M))"
proof
fix t assume "t ∈ (⋃((set ∘ fst ∘ Ana) ` M))"
then obtain s where s: "s ∈ M" "t ∈ (set ∘ fst ∘ Ana) s" by blast
obtain K R where KR: "Ana s = (K,R)" by (metis surj_pair)
hence "t ∈ set K" using s(2) by simp
thus "wf⇩t⇩r⇩m t" using Ana_keys_wf'[OF KR] wf_M s(1) by blast
qed
show ?case using Ana_subst'_or_Ana_keys_subterm
proof
assume "∀t K T k. Ana t = (K, T) ⟶ k ∈ set K ⟶ k ⊏ t"
hence *: "k ⊑ t" using Ana.hyps(2,3) by auto
show ?thesis by (rule SMP_D_aux3[OF * wf_t Ana.prems Ana.IH[OF 1] M_SMP_repr])
next
assume Ana_subst':
"∀f T δ K M. Ana (Fun f T) = (K, M) ⟶ Ana (Fun f T ⋅ δ) = (K ⋅⇩l⇩i⇩s⇩t δ, M ⋅⇩l⇩i⇩s⇩t δ)"
have "arity f > 0" using Ana_const[of f U] U Ana.hyps(2,3) by fastforce
hence "U ≠ []" using wf_t U unfolding wf⇩t⇩r⇩m_def by force
then obtain m δ where m: "m ∈ M" "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)" "t = m ⋅ δ" "is_Fun m"
using Ana.IH[OF 1] U by auto
hence "Ana (t ⋅ δ) = (K ⋅⇩l⇩i⇩s⇩t δ,T ⋅⇩l⇩i⇩s⇩t δ)" using Ana_subst' U Ana.hyps(2) by auto
obtain Km Tm where Ana_m: "Ana m = (Km,Tm)" by atomize_elim auto
hence "Ana (m ⋅ δ) = (Km ⋅⇩l⇩i⇩s⇩t δ,Tm ⋅⇩l⇩i⇩s⇩t δ)"
using Ana_subst' U m(4) is_FunE[OF m(5)] Ana.hyps(2)
by metis
then obtain km where km: "km ∈ set Km" "k = km ⋅ δ" using Ana.hyps(2,3) m(4) by auto
then obtain θ km' where θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
and km': "km' ∈ M" "km = km' ⋅ θ"
using Ana_m m(1) has_all_wt_instances_ofD'[OF wf_M_keys wf_M closed(2), of km] by force
have kθδ: "k = km' ⋅ θ ∘⇩s δ" "wt⇩s⇩u⇩b⇩s⇩t (θ ∘⇩s δ)" "wf⇩t⇩r⇩m⇩s (subst_range (θ ∘⇩s δ))"
using km(2) km' wt_subst_compose[OF θ(1) m(2)] wf_trms_subst_compose[OF θ(2) m(3)]
by auto
show ?case
proof (cases "is_Fun km'")
case True thus ?thesis using kθδ km'(1) by blast
next
case False
note F = False
then obtain x where x: "km' = Var x" by auto
hence 3: "x ∈ fv⇩s⇩e⇩t M" using fv_subset[OF km'(1)] by auto
obtain kf kT where kf: "k = Fun kf kT" using Ana.prems by auto
show ?thesis
proof (cases "kT = []")
case True thus ?thesis using kθδ(1) kθδ(2) kθδ(3) kf km'(1) by blast
next
case False
hence 4: "arity kf > 0" using wf_k kf TAtom_term_cases const_type by fastforce
then obtain kT' where kT': "Γ k = TComp kf kT'" by (simp add: fun_type kf)
then obtain V where V:
"Fun kf V ∈ M" "Γ (Fun kf V) = Γ (Var x)" "∀u ∈ set V. ∃v. u = Var v"
"distinct V" "is_Fun (Fun kf V)"
using is_TComp_var_instance_closedD[OF _ _ closed(3), of x]
x m(2) kθδ(1) 3 wt_subst_trm''[OF kθδ(2)]
by (metis fun_type_id_eq term.disc(2) is_VarE)
have 5: "kT' = map Γ V"
using fun_type[OF 4] x kT' kθδ m(2) V(2)
by (metis term.inject(2) wt_subst_trm'')
thus ?thesis
using TComp_var_instance_wt_subst_exists wf_k kf 4 V(3,4) kT' V(1,5)
by metis
qed
qed
qed
qed
qed
lemma SMP_D':
fixes M
defines "δ ≡ var_rename (max_var_set (fv⇩s⇩e⇩t M))"
assumes M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
and s: "s ∈ SMP M" "is_Fun s" "∄f. s = Fun f []"
and t: "t ∈ SMP M" "is_Fun t" "∄f. t = Fun f []"
obtains σ s0 θ t0
where "wt⇩s⇩u⇩b⇩s⇩t σ" "wf⇩t⇩r⇩m⇩s (subst_range σ)" "s0 ∈ M" "is_Fun s0" "s = s0 ⋅ σ" "Γ s = Γ s0"
and "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "t0 ∈ M" "is_Fun t0" "t = t0 ⋅ δ ⋅ θ" "Γ t = Γ t0"
proof -
obtain σ s0 where
s0: "wt⇩s⇩u⇩b⇩s⇩t σ" "wf⇩t⇩r⇩m⇩s (subst_range σ)" "s0 ∈ M" "s = s0 ⋅ σ" "is_Fun s0"
using s(3) SMP_D[OF s(1,2) M_SMP_repr] unfolding δ_def by metis
obtain θ t0 where t0:
"wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "t0 ∈ M" "t = t0 ⋅ δ ⋅ θ" "is_Fun t0"
using t(3) SMP_D[OF t(1,2) M_SMP_repr] var_rename_wt'[of _ t]
wf_trms_subst_compose_Var_range(1)[OF _ var_rename_is_renaming(2)]
unfolding δ_def by metis
have "Γ s = Γ s0" "Γ t = Γ (t0 ⋅ δ)" "Γ (t0 ⋅ δ) = Γ t0"
using s0 t0 wt_subst_trm'' by (metis, metis, metis δ_def var_rename_wt(1))
thus ?thesis using s0 t0 that by simp
qed
lemma SMP_D'':
fixes t::"('fun, ('fun, 'atom) term × nat) term"
assumes t_SMP: "t ∈ SMP M"
and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
shows "∃m ∈ M. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = m ⋅ δ"
proof (cases "(∃x. t = Var x) ∨ (∃c. t = Fun c [])")
case True
have M_wf: "wf⇩t⇩r⇩m⇩s M"
and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
and M_subterms_cl: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
using finite_SMP_representationD[OF M_SMP_repr] by blast+
have M_Ana_wf: "wf⇩t⇩r⇩m⇩s (⋃ ((set ∘ fst ∘ Ana) ` M))"
proof
fix k assume "k ∈ ⋃((set ∘ fst ∘ Ana) ` M)"
then obtain m where m: "m ∈ M" "k ∈ set (fst (Ana m))" by force
thus "wf⇩t⇩r⇩m k" using M_wf Ana_keys_wf'[of m "fst (Ana m)" _ k] surjective_pairing by blast
qed
show ?thesis using True
proof
assume "∃x. t = Var x"
then obtain x y where x: "t = Var x" and y: "y ∈ fv⇩s⇩e⇩t M" "Γ (Var y) = Γ (Var x)"
using SMP_D_aux1[OF t_SMP M_subterms_cl M_var_inst_cl M_wf] by fastforce
then obtain m δ where m: "m ∈ M" "m ⋅ δ = Var y" and δ: "wt⇩s⇩u⇩b⇩s⇩t δ"
using has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl, of "Var y"]
vars_iff_subtermeq_set[of y M]
by fastforce
obtain z where z: "m = Var z" using m(2) by (cases m) auto
define θ where "θ ≡ Var(z := Var x)::('fun, ('fun, 'atom) term × nat) subst"
have "Γ (Var z) = Γ (Var x)" using y(2) m(2) z wt_subst_trm''[OF δ, of m] by argo
hence "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" unfolding θ_def wt⇩s⇩u⇩b⇩s⇩t_def by force+
moreover have "t = m ⋅ θ" using x z unfolding θ_def by simp
ultimately show ?thesis using m(1) by blast
qed (use SMP_D[OF t_SMP _ M_SMP_repr] in blast)
qed (use SMP_D[OF t_SMP _ M_SMP_repr] in blast)
end
lemma tfr⇩s⇩e⇩t_if_comp_tfr⇩s⇩e⇩t:
assumes "comp_tfr⇩s⇩e⇩t arity Ana Γ M"
shows "tfr⇩s⇩e⇩t M"
proof -
let ?δ = "var_rename (max_var_set (fv⇩s⇩e⇩t M))"
have M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
by (metis comp_tfr⇩s⇩e⇩t_def assms)
have M_finite: "finite M"
using assms card_gt_0_iff unfolding comp_tfr⇩s⇩e⇩t_def finite_SMP_representation_def by blast
show ?thesis
proof (unfold tfr⇩s⇩e⇩t_def; intro ballI impI)
fix s t assume "s ∈ SMP M - Var`𝒱" "t ∈ SMP M - Var`𝒱"
hence st: "s ∈ SMP M" "is_Fun s" "t ∈ SMP M" "is_Fun t" by auto
have "¬(∃δ. Unifier δ s t)" when st_type_neq: "Γ s ≠ Γ t"
proof (cases "∃f. s = Fun f [] ∨ t = Fun f []")
case False
then obtain σ s0 θ t0 where
s0: "s0 ∈ M" "is_Fun s0" "s = s0 ⋅ σ" "Γ s = Γ s0"
and t0: "t0 ∈ M" "is_Fun t0" "t = t0 ⋅ ?δ ⋅ θ" "Γ t = Γ t0"
using SMP_D'[OF M_SMP_repr st(1,2) _ st(3,4)] by metis
hence "¬(∃δ. Unifier δ s0 (t0 ⋅ ?δ))"
using assms mgu_None_is_subst_neq st_type_neq wt_subst_trm''[OF var_rename_wt(1)]
unfolding comp_tfr⇩s⇩e⇩t_def Let_def by metis
thus ?thesis
using vars_term_disjoint_imp_unifier[OF var_rename_fv_set_disjoint[OF M_finite]] s0(1) t0(1)
unfolding s0(3) t0(3) by (metis (no_types, opaque_lifting) subst_subst_compose)
qed (use st_type_neq st(2,4) in auto)
thus "Γ s = Γ t" when "∃δ. Unifier δ s t" by (metis that)
qed
qed
lemma tfr⇩s⇩e⇩t_if_comp_tfr⇩s⇩e⇩t':
assumes "let N = SMP0 Ana Γ M in set M ⊆ set N ∧ comp_tfr⇩s⇩e⇩t arity Ana Γ (set N)"
shows "tfr⇩s⇩e⇩t (set M)"
by (rule tfr_subset(2)[
OF tfr⇩s⇩e⇩t_if_comp_tfr⇩s⇩e⇩t[OF conjunct2[OF assms[unfolded Let_def]]]
conjunct1[OF assms[unfolded Let_def]]])
lemma tfr⇩s⇩t⇩p_is_comp_tfr⇩s⇩t⇩p: "tfr⇩s⇩t⇩p a = comp_tfr⇩s⇩t⇩p Γ a"
proof (cases a)
case (Equality ac t t')
thus ?thesis
using mgu_always_unifies[of t _ t'] mgu_gives_MGU[of t t']
by auto
next
case (Inequality X F)
thus ?thesis
using tfr⇩s⇩t⇩p.simps(2)[of X F]
comp_tfr⇩s⇩t⇩p.simps(2)[of Γ X F]
Fun_range_case(2)[of "subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F)"]
unfolding is_Var_def
by auto
qed auto
lemma tfr⇩s⇩t_if_comp_tfr⇩s⇩t:
assumes "comp_tfr⇩s⇩t arity Ana Γ M S"
shows "tfr⇩s⇩t S"
unfolding tfr⇩s⇩t_def
proof
have comp_tfr⇩s⇩e⇩t_M: "comp_tfr⇩s⇩e⇩t arity Ana Γ M"
using assms unfolding comp_tfr⇩s⇩t_def by blast
have wf⇩t⇩r⇩m⇩s_M: "wf⇩t⇩r⇩m⇩s M"
and wf⇩t⇩r⇩m⇩s_S: "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)"
and S_trms_instance_M: "has_all_wt_instances_of Γ (trms⇩s⇩t S) M"
using assms wf⇩t⇩r⇩m_code wf⇩t⇩r⇩m⇩s_code trms_list⇩s⇩t_is_trms⇩s⇩t
unfolding comp_tfr⇩s⇩t_def comp_tfr⇩s⇩e⇩t_def finite_SMP_representation_def list_all_iff
by blast+
show "tfr⇩s⇩e⇩t (trms⇩s⇩t S)"
using tfr_subset(3)[OF tfr⇩s⇩e⇩t_if_comp_tfr⇩s⇩e⇩t[OF comp_tfr⇩s⇩e⇩t_M] SMP_SMP_subset]
SMP_I'[OF wf⇩t⇩r⇩m⇩s_S wf⇩t⇩r⇩m⇩s_M S_trms_instance_M]
by blast
have "list_all (comp_tfr⇩s⇩t⇩p Γ) S" by (metis assms comp_tfr⇩s⇩t_def)
thus "list_all tfr⇩s⇩t⇩p S" by (induct S) (simp_all add: tfr⇩s⇩t⇩p_is_comp_tfr⇩s⇩t⇩p)
qed
lemma tfr⇩s⇩t_if_comp_tfr⇩s⇩t':
assumes "comp_tfr⇩s⇩t arity Ana Γ (set (SMP0 Ana Γ (trms_list⇩s⇩t S))) S"
shows "tfr⇩s⇩t S"
by (rule tfr⇩s⇩t_if_comp_tfr⇩s⇩t[OF assms])
subsubsection ‹Lemmata for Checking Ground SMP (GSMP) Disjointness›
context
begin
private lemma ground_SMP_disjointI_aux1:
fixes M::"('fun, ('fun, 'atom) term × nat) term set"
assumes f_def: "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
and g_def: "g ≡ λM. {t ∈ M. fv t = {}}"
shows "f (SMP M) = g (SMP M)"
proof
have "t ∈ f (SMP M)" when t: "t ∈ SMP M" "fv t = {}" for t
proof -
define δ where "δ ≡ Var::('fun, ('fun, 'atom) term × nat) subst"
have "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)" "t = t ⋅ δ"
using subst_apply_term_empty[of t] that(2) wt_subst_Var wf_trm_subst_range_Var
unfolding δ_def by auto
thus ?thesis using SMP.Substitution[OF t(1), of δ] t(2) unfolding f_def by fastforce
qed
thus "g (SMP M) ⊆ f (SMP M)" unfolding g_def by blast
qed (use f_def g_def in blast)
private lemma ground_SMP_disjointI_aux2:
fixes M::"('fun, ('fun, 'atom) term × nat) term set"
assumes f_def: "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
shows "f M = f (SMP M)"
proof
have M_wf: "wf⇩t⇩r⇩m⇩s M"
and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
and M_subterms_cl: "has_all_wt_instances_of Γ (subterms⇩s⇩e⇩t M) M"
and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
using finite_SMP_representationD[OF M_SMP_repr] by blast+
show "f (SMP M) ⊆ f M"
proof
fix t assume "t ∈ f (SMP M)"
then obtain s δ where s: "t = s ⋅ δ" "s ∈ SMP M" "fv (s ⋅ δ) = {}"
and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
unfolding f_def by blast
have t_wf: "wf⇩t⇩r⇩m t" using SMP_wf_trm[OF s(2) M_wf] s(1) wf_trm_subst[OF δ(2)] by blast
obtain m θ where m: "m ∈ M" "s = m ⋅ θ" and θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
using SMP_D''[OF s(2) M_SMP_repr] by blast
have "t = m ⋅ (θ ∘⇩s δ)" "fv (m ⋅ (θ ∘⇩s δ)) = {}" using s(1,3) m(2) by simp_all
thus "t ∈ f M"
using m(1) wt_subst_compose[OF θ(1) δ(1)] wf_trms_subst_compose[OF θ(2) δ(2)]
unfolding f_def by blast
qed
qed (auto simp add: f_def)
private lemma ground_SMP_disjointI_aux3:
fixes A B C::"('fun, ('fun, 'atom) term × nat) term set"
defines "P ≡ λt s. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ Unifier δ t s"
assumes f_def: "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
and Q_def: "Q ≡ λt. intruder_synth' public arity {} t"
and R_def: "R ≡ λt. ∃u ∈ C. is_wt_instance_of_cond Γ t u"
and AB: "wf⇩t⇩r⇩m⇩s A" "wf⇩t⇩r⇩m⇩s B" "fv⇩s⇩e⇩t A ∩ fv⇩s⇩e⇩t B = {}"
and C: "wf⇩t⇩r⇩m⇩s C"
and ABC: "∀t ∈ A. ∀s ∈ B. P t s ⟶ Q t ∨ R t"
shows "f A ∩ f B ⊆ f C ∪ {m. {} ⊢⇩c m}"
proof
fix t assume "t ∈ f A ∩ f B"
then obtain ta tb δa δb where
ta: "t = ta ⋅ δa" "ta ∈ A" "wt⇩s⇩u⇩b⇩s⇩t δa" "wf⇩t⇩r⇩m⇩s (subst_range δa)" "fv (ta ⋅ δa) = {}"
and tb: "t = tb ⋅ δb" "tb ∈ B" "wt⇩s⇩u⇩b⇩s⇩t δb" "wf⇩t⇩r⇩m⇩s (subst_range δb)" "fv (tb ⋅ δb) = {}"
unfolding f_def by blast
have ta_tb_wf: "wf⇩t⇩r⇩m ta" "wf⇩t⇩r⇩m tb" "fv ta ∩ fv tb = {}" "Γ ta = Γ tb"
using ta(1,2) tb(1,2) AB fv_subset_subterms
wt_subst_trm''[OF ta(3), of ta] wt_subst_trm''[OF tb(3), of tb]
by (fast, fast, blast, simp)
obtain θ where θ: "Unifier θ ta tb" "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
using vars_term_disjoint_imp_unifier[OF ta_tb_wf(3), of δa δb]
ta(1) tb(1) wt_Unifier_if_Unifier[OF ta_tb_wf(1,2,4)]
by blast
hence "Q ta ∨ R ta" using ABC ta(2) tb(2) unfolding P_def by blast+
thus "t ∈ f C ∪ {m. {} ⊢⇩c m}"
proof
show "Q ta ⟹ ?thesis"
using ta(1) pgwt_ground[of ta] pgwt_is_empty_synth[of ta] subst_ground_ident[of ta δa]
unfolding Q_def f_def intruder_synth_code[symmetric] by simp
next
assume "R ta"
then obtain ua σa where ua: "ta = ua ⋅ σa" "ua ∈ C" "wt⇩s⇩u⇩b⇩s⇩t σa" "wf⇩t⇩r⇩m⇩s (subst_range σa)"
using θ ABC ta_tb_wf(1,2) ta(2) tb(2) C is_wt_instance_of_condD'
unfolding P_def R_def by metis
have "t = ua ⋅ (σa ∘⇩s δa)" "fv t = {}"
using ua(1) ta(1,5) tb(1,5) by auto
thus ?thesis
using ua(2) wt_subst_compose[OF ua(3) ta(3)] wf_trms_subst_compose[OF ua(4) ta(4)]
unfolding f_def by blast
qed
qed
lemma ground_SMP_disjointI:
fixes A B::"('fun, ('fun, 'atom) term × nat) term set" and C
defines "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
and "g ≡ λM. {t ∈ M. fv t = {}}"
and "Q ≡ λt. intruder_synth' public arity {} t"
and "R ≡ λt. ∃u ∈ C. is_wt_instance_of_cond Γ t u"
assumes AB_fv_disj: "fv⇩s⇩e⇩t A ∩ fv⇩s⇩e⇩t B = {}"
and A_SMP_repr: "finite_SMP_representation arity Ana Γ A"
and B_SMP_repr: "finite_SMP_representation arity Ana Γ B"
and C_wf: "wf⇩t⇩r⇩m⇩s C"
and ABC: "∀t ∈ A. ∀s ∈ B. Γ t = Γ s ∧ mgu t s ≠ None ⟶ Q t ∨ R t"
shows "g (SMP A) ∩ g (SMP B) ⊆ f C ∪ {m. {} ⊢⇩c m}"
proof -
have AB_wf: "wf⇩t⇩r⇩m⇩s A" "wf⇩t⇩r⇩m⇩s B"
using A_SMP_repr B_SMP_repr finite_SMP_representationD(1)
by (blast, blast)
let ?P = "λt s. ∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ Unifier δ t s"
have ABC': "∀t ∈ A. ∀s ∈ B. ?P t s ⟶ Q t ∨ R t"
by (metis (no_types) ABC mgu_None_is_subst_neq wt_subst_trm'')
show ?thesis
using ground_SMP_disjointI_aux1[OF f_def g_def, of A]
ground_SMP_disjointI_aux1[OF f_def g_def, of B]
ground_SMP_disjointI_aux2[OF f_def A_SMP_repr]
ground_SMP_disjointI_aux2[OF f_def B_SMP_repr]
ground_SMP_disjointI_aux3[OF f_def Q_def R_def AB_wf AB_fv_disj C_wf ABC']
by argo
qed
end
end
end