Theory Term_Implication
section‹Term Implication›
theory Term_Implication
imports Stateful_Protocol_Model Term_Variants
begin
subsection ‹Single Term Implications›
definition timpl_apply_term ("⟨_ --» _⟩⟨_⟩") where
"⟨a --» b⟩⟨t⟩ ≡ term_variants ((λ_. [])(Abs a := [Abs b])) t"
definition timpl_apply_terms ("⟨_ --» _⟩⟨_⟩⇩s⇩e⇩t") where
"⟨a --» b⟩⟨M⟩⇩s⇩e⇩t ≡ ⋃((set o timpl_apply_term a b) ` M)"
lemma timpl_apply_Fun:
assumes "⋀i. i < length T ⟹ S ! i ∈ set ⟨a --» b⟩⟨T ! i⟩"
and "length T = length S"
shows "Fun f S ∈ set ⟨a --» b⟩⟨Fun f T⟩"
using assms term_variants_Fun term_variants_pred_iff_in_term_variants
by (metis timpl_apply_term_def)
lemma timpl_apply_Abs:
assumes "⋀i. i < length T ⟹ S ! i ∈ set ⟨a --» b⟩⟨T ! i⟩"
and "length T = length S"
shows "Fun (Abs b) S ∈ set ⟨a --» b⟩⟨Fun (Abs a) T⟩"
using assms(1) term_variants_P[OF assms(2), of "(λ_. [])(Abs a := [Abs b])" "Abs b" "Abs a"]
unfolding timpl_apply_term_def term_variants_pred_iff_in_term_variants[symmetric]
by fastforce
lemma timpl_apply_refl: "t ∈ set ⟨a --» b⟩⟨t⟩"
unfolding timpl_apply_term_def
by (metis term_variants_pred_refl term_variants_pred_iff_in_term_variants)
lemma timpl_apply_const: "Fun (Abs b) [] ∈ set ⟨a --» b⟩⟨Fun (Abs a) []⟩"
using term_variants_pred_iff_in_term_variants term_variants_pred_const
unfolding timpl_apply_term_def by auto
lemma timpl_apply_const':
"c = a ⟹ set ⟨a --» b⟩⟨Fun (Abs c) []⟩ = {Fun (Abs b) [], Fun (Abs c) []}"
"c ≠ a ⟹ set ⟨a --» b⟩⟨Fun (Abs c) []⟩ = {Fun (Abs c) []}"
using term_variants_pred_const_cases[of "(λ_. [])(Abs a := [Abs b])" "Abs c"]
term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
unfolding timpl_apply_term_def by auto
lemma timpl_apply_term_subst:
"s ∈ set ⟨a --» b⟩⟨t⟩ ⟹ s ⋅ δ ∈ set ⟨a --» b⟩⟨t ⋅ δ⟩"
by (metis term_variants_pred_iff_in_term_variants term_variants_pred_subst timpl_apply_term_def)
lemma timpl_apply_inv:
assumes "Fun h S ∈ set ⟨a --» b⟩⟨Fun f T⟩"
shows "length T = length S"
and "⋀i. i < length T ⟹ S ! i ∈ set ⟨a --» b⟩⟨T ! i⟩"
and "f ≠ h ⟹ f = Abs a ∧ h = Abs b"
using assms term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
unfolding timpl_apply_term_def
by (metis (full_types) term_variants_pred_inv(1),
metis (full_types) term_variants_pred_inv(2),
fastforce dest: term_variants_pred_inv(3))
lemma timpl_apply_inv':
assumes "s ∈ set ⟨a --» b⟩⟨Fun f T⟩"
shows "∃g S. s = Fun g S"
proof -
have *: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) (Fun f T) s"
using assms term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
unfolding timpl_apply_term_def by force
show ?thesis using term_variants_pred.cases[OF *, of ?thesis] by fastforce
qed
lemma timpl_apply_term_Var_iff:
"Var x ∈ set ⟨a --» b⟩⟨t⟩ ⟷ t = Var x"
using term_variants_pred_inv_Var term_variants_pred_iff_in_term_variants
unfolding timpl_apply_term_def by metis
subsection ‹Term Implication Closure›
inductive_set timpl_closure for t TI where
FP: "t ∈ timpl_closure t TI"
| TI: "⟦u ∈ timpl_closure t TI; (a,b) ∈ TI; term_variants_pred ((λ_. [])(Abs a := [Abs b])) u s⟧
⟹ s ∈ timpl_closure t TI"
definition "timpl_closure_set M TI ≡ (⋃t ∈ M. timpl_closure t TI)"
inductive_set timpl_closure'_step for TI where
"⟦(a,b) ∈ TI; term_variants_pred ((λ_. [])(Abs a := [Abs b])) t s⟧
⟹ (t,s) ∈ timpl_closure'_step TI"
definition "timpl_closure' TI ≡ (timpl_closure'_step TI)⇧*"
definition comp_timpl_closure where
"comp_timpl_closure FP TI ≡
let f = λX. FP ∪ (⋃x ∈ X. ⋃(a,b) ∈ TI. set ⟨a --» b⟩⟨x⟩)
in while (λX. f X ≠ X) f {}"
definition comp_timpl_closure_list where
"comp_timpl_closure_list FP TI ≡
let f = λX. remdups (concat (map (λx. concat (map (λ(a,b). ⟨a --» b⟩⟨x⟩) TI)) X)@X)
in while (λX. set (f X) ≠ set X) f FP"
lemma timpl_closure_setI:
"t ∈ M ⟹ t ∈ timpl_closure_set M TI"
unfolding timpl_closure_set_def by (auto intro: timpl_closure.FP)
lemma timpl_closure_set_empty_timpls:
"timpl_closure t {} = {t}" (is "?A = ?B")
proof (intro subset_antisym subsetI)
fix s show "s ∈ ?A ⟹ s ∈ ?B"
by (induct s rule: timpl_closure.induct) auto
qed (simp add: timpl_closure.FP)
lemmas timpl_closure_set_is_timpl_closure_union = meta_eq_to_obj_eq[OF timpl_closure_set_def]
lemma term_variants_pred_eq_case_Abs:
fixes a b
defines "P ≡ (λ_. [])(Abs a := [Abs b])"
assumes "term_variants_pred P t s" "∀f ∈ funs_term s. ¬is_Abs f"
shows "t = s"
using assms(2,3)
proof (induction t s rule: term_variants_pred.induct)
case (term_variants_Fun T S f)
have "¬is_Abs h" when i: "i < length S" and h: "h ∈ funs_term (S ! i)" for i h
using i h term_variants_Fun.prems by auto
hence "T ! i = S ! i" when i: "i < length T" for i
using i term_variants_Fun.hyps(1) term_variants_Fun.IH by auto
hence "T = S" using term_variants_Fun.hyps(1) nth_equalityI[of T S] by fast
thus ?case using term_variants_Fun.hyps(1) by blast
qed (simp_all add: term_variants_pred_refl P_def)
lemma timpl_closure'_step_inv:
assumes "(t,s) ∈ timpl_closure'_step TI"
obtains a b where "(a,b) ∈ TI" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) t s"
using assms by (auto elim: timpl_closure'_step.cases)
lemma timpl_closure_mono:
assumes "TI ⊆ TI'"
shows "timpl_closure t TI ⊆ timpl_closure t TI'"
proof
fix s show "s ∈ timpl_closure t TI ⟹ s ∈ timpl_closure t TI'"
apply (induct rule: timpl_closure.induct)
using assms by (auto intro: timpl_closure.intros)
qed
lemma timpl_closure_set_mono:
assumes "M ⊆ M'" "TI ⊆ TI'"
shows "timpl_closure_set M TI ⊆ timpl_closure_set M' TI'"
using assms(1) timpl_closure_mono[OF assms(2)] unfolding timpl_closure_set_def by fast
lemma timpl_closure_idem:
"timpl_closure_set (timpl_closure t TI) TI = timpl_closure t TI" (is "?A = ?B")
proof
have "s ∈ timpl_closure t TI"
when "s ∈ timpl_closure u TI" "u ∈ timpl_closure t TI"
for s u
using that
by (induction rule: timpl_closure.induct)
(auto intro: timpl_closure.intros)
thus "?A ⊆ ?B" unfolding timpl_closure_set_def by blast
show "?B ⊆ ?A"
unfolding timpl_closure_set_def
by (blast intro: timpl_closure.FP)
qed
lemma timpl_closure_set_idem:
"timpl_closure_set (timpl_closure_set M TI) TI = timpl_closure_set M TI"
using timpl_closure_idem[of _ TI]unfolding timpl_closure_set_def by auto
lemma timpl_closure_set_mono_timpl_closure_set:
assumes N: "N ⊆ timpl_closure_set M TI"
shows "timpl_closure_set N TI ⊆ timpl_closure_set M TI"
using timpl_closure_set_mono[OF N, of TI TI] timpl_closure_set_idem[of M TI]
by simp
lemma timpl_closure_is_timpl_closure':
"s ∈ timpl_closure t TI ⟷ (t,s) ∈ timpl_closure' TI"
proof
show "s ∈ timpl_closure t TI ⟹ (t,s) ∈ timpl_closure' TI"
unfolding timpl_closure'_def
by (induct rule: timpl_closure.induct)
(auto intro: rtrancl_into_rtrancl timpl_closure'_step.intros)
show "(t,s) ∈ timpl_closure' TI ⟹ s ∈ timpl_closure t TI"
unfolding timpl_closure'_def
by (induct rule: rtrancl_induct)
(auto dest: timpl_closure'_step_inv
intro: timpl_closure.FP timpl_closure.TI)
qed
lemma timpl_closure'_mono:
assumes "TI ⊆ TI'"
shows "timpl_closure' TI ⊆ timpl_closure' TI'"
using timpl_closure_mono[OF assms]
timpl_closure_is_timpl_closure'[of _ _ TI]
timpl_closure_is_timpl_closure'[of _ _ TI']
by fast
lemma timpl_closureton_is_timpl_closure:
"timpl_closure_set {t} TI = timpl_closure t TI"
by (simp add: timpl_closure_set_is_timpl_closure_union)
lemma timpl_closure'_timpls_trancl_subset:
"timpl_closure' (c⇧+) ⊆ timpl_closure' c"
unfolding timpl_closure'_def
proof
fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
show "(s,t) ∈ (timpl_closure'_step (c⇧+))⇧* ⟹ (s,t) ∈ (timpl_closure'_step c)⇧*"
proof (induction rule: rtrancl_induct)
case (step u t)
obtain a b where ab:
"(a,b) ∈ c⇧+" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
using step.hyps(2) timpl_closure'_step_inv by blast
hence "(u,t) ∈ (timpl_closure'_step c)⇧*"
proof (induction arbitrary: t rule: trancl_induct)
case (step d e)
obtain s where s:
"term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
"term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast
have "(u,s) ∈ (timpl_closure'_step c)⇧*"
"(s,t) ∈ timpl_closure'_step c"
using step.hyps(2) s(2) step.IH[OF s(1)]
by (auto intro: timpl_closure'_step.intros)
thus ?case by simp
qed (auto intro: timpl_closure'_step.intros)
thus ?case using step.IH by simp
qed simp
qed
lemma timpl_closure'_timpls_trancl_subset':
"timpl_closure' {(a,b) ∈ c⇧+. a ≠ b} ⊆ timpl_closure' c"
using timpl_closure'_timpls_trancl_subset
timpl_closure'_mono[of "{(a,b) ∈ c⇧+. a ≠ b}" "c⇧+"]
by fast
lemma timpl_closure_set_timpls_trancl_subset:
"timpl_closure_set M (c⇧+) ⊆ timpl_closure_set M c"
using timpl_closure'_timpls_trancl_subset[of c]
timpl_closure_is_timpl_closure'[of _ _ c]
timpl_closure_is_timpl_closure'[of _ _ "c⇧+"]
timpl_closure_set_is_timpl_closure_union[of M c]
timpl_closure_set_is_timpl_closure_union[of M "c⇧+"]
by fastforce
lemma timpl_closure_set_timpls_trancl_subset':
"timpl_closure_set M {(a,b) ∈ c⇧+. a ≠ b} ⊆ timpl_closure_set M c"
using timpl_closure'_timpls_trancl_subset'[of c]
timpl_closure_is_timpl_closure'[of _ _ c]
timpl_closure_is_timpl_closure'[of _ _ "{(a,b) ∈ c⇧+. a ≠ b}"]
timpl_closure_set_is_timpl_closure_union[of M c]
timpl_closure_set_is_timpl_closure_union[of M "{(a,b) ∈ c⇧+. a ≠ b}"]
by fastforce
lemma timpl_closure'_timpls_trancl_supset':
"timpl_closure' c ⊆ timpl_closure' {(a,b) ∈ c⇧+. a ≠ b}"
unfolding timpl_closure'_def
proof
let ?cl = "{(a,b) ∈ c⇧+. a ≠ b}"
fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
show "(s,t) ∈ (timpl_closure'_step c)⇧* ⟹ (s,t) ∈ (timpl_closure'_step ?cl)⇧*"
proof (induction rule: rtrancl_induct)
case (step u t)
obtain a b where ab:
"(a,b) ∈ c" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
using step.hyps(2) timpl_closure'_step_inv by blast
hence "(a,b) ∈ c⇧+" by simp
hence "(u,t) ∈ (timpl_closure'_step ?cl)⇧*" using ab(2)
proof (induction arbitrary: t rule: trancl_induct)
case (base d) show ?case
proof (cases "a = d")
case True thus ?thesis
using base term_variants_pred_refl_inv[of _ u t]
by force
next
case False thus ?thesis
using base timpl_closure'_step.intros[of a d ?cl]
by fast
qed
next
case (step d e)
obtain s where s:
"term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
"term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast
show ?case
proof (cases "d = e")
case True
thus ?thesis
using step.prems step.IH[of t]
by blast
next
case False
hence "(u,s) ∈ (timpl_closure'_step ?cl)⇧*"
"(s,t) ∈ timpl_closure'_step ?cl"
using step.hyps(2) s(2) step.IH[OF s(1)]
by (auto intro: timpl_closure'_step.intros)
thus ?thesis by simp
qed
qed
thus ?case using step.IH by simp
qed simp
qed
lemma timpl_closure'_timpls_trancl_supset:
"timpl_closure' c ⊆ timpl_closure' (c⇧+)"
using timpl_closure'_timpls_trancl_supset'[of c]
timpl_closure'_mono[of "{(a,b) ∈ c⇧+. a ≠ b}" "c⇧+"]
by fast
lemma timpl_closure'_timpls_trancl_eq:
"timpl_closure' (c⇧+) = timpl_closure' c"
using timpl_closure'_timpls_trancl_subset timpl_closure'_timpls_trancl_supset
by blast
lemma timpl_closure'_timpls_trancl_eq':
"timpl_closure' {(a,b) ∈ c⇧+. a ≠ b} = timpl_closure' c"
using timpl_closure'_timpls_trancl_subset' timpl_closure'_timpls_trancl_supset'
by blast
lemma timpl_closure'_timpls_rtrancl_subset:
"timpl_closure' (c⇧*) ⊆ timpl_closure' c"
unfolding timpl_closure'_def
proof
fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
show "(s,t) ∈ (timpl_closure'_step (c⇧*))⇧* ⟹ (s,t) ∈ (timpl_closure'_step c)⇧*"
proof (induction rule: rtrancl_induct)
case (step u t)
obtain a b where ab:
"(a,b) ∈ c⇧*" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
using step.hyps(2) timpl_closure'_step_inv by blast
hence "(u,t) ∈ (timpl_closure'_step c)⇧*"
proof (induction arbitrary: t rule: rtrancl_induct)
case base
hence "u = t" using term_variants_pred_refl_inv by fastforce
thus ?case by simp
next
case (step d e)
obtain s where s:
"term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
"term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast
have "(u,s) ∈ (timpl_closure'_step c)⇧*"
"(s,t) ∈ timpl_closure'_step c"
using step.hyps(2) s(2) step.IH[OF s(1)]
by (auto intro: timpl_closure'_step.intros)
thus ?case by simp
qed
thus ?case using step.IH by simp
qed simp
qed
lemma timpl_closure'_timpls_rtrancl_supset:
"timpl_closure' c ⊆ timpl_closure' (c⇧*)"
unfolding timpl_closure'_def
proof
fix s t::"(('a,'b,'c,'d) prot_fun,'e) term"
show "(s,t) ∈ (timpl_closure'_step c)⇧* ⟹ (s,t) ∈ (timpl_closure'_step (c⇧*))⇧*"
proof (induction rule: rtrancl_induct)
case (step u t)
obtain a b where ab:
"(a,b) ∈ c" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u t"
using step.hyps(2) timpl_closure'_step_inv by blast
hence "(a,b) ∈ c⇧*" by simp
hence "(u,t) ∈ (timpl_closure'_step (c⇧*))⇧*" using ab(2)
proof (induction arbitrary: t rule: rtrancl_induct)
case (base t) thus ?case using term_variants_pred_refl_inv[of _ u t] by fastforce
next
case (step d e)
obtain s where s:
"term_variants_pred ((λ_. [])(Abs a := [Abs d])) u s"
"term_variants_pred ((λ_. [])(Abs d := [Abs e])) s t"
using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast
show ?case
proof (cases "d = e")
case True
thus ?thesis
using step.prems step.IH[of t]
by blast
next
case False
hence "(u,s) ∈ (timpl_closure'_step (c⇧*))⇧*"
"(s,t) ∈ timpl_closure'_step (c⇧*)"
using step.hyps(2) s(2) step.IH[OF s(1)]
by (auto intro: timpl_closure'_step.intros)
thus ?thesis by simp
qed
qed
thus ?case using step.IH by simp
qed simp
qed
lemma timpl_closure'_timpls_rtrancl_eq:
"timpl_closure' (c⇧*) = timpl_closure' c"
using timpl_closure'_timpls_rtrancl_subset timpl_closure'_timpls_rtrancl_supset
by blast
lemma timpl_closure_timpls_trancl_eq:
"timpl_closure t (c⇧+) = timpl_closure t c"
using timpl_closure'_timpls_trancl_eq[of c]
timpl_closure_is_timpl_closure'[of _ _ c]
timpl_closure_is_timpl_closure'[of _ _ "c⇧+"]
by fastforce
lemma timpl_closure_set_timpls_trancl_eq:
"timpl_closure_set M (c⇧+) = timpl_closure_set M c"
using timpl_closure_timpls_trancl_eq
timpl_closure_set_is_timpl_closure_union[of M c]
timpl_closure_set_is_timpl_closure_union[of M "c⇧+"]
by fastforce
lemma timpl_closure_set_timpls_trancl_eq':
"timpl_closure_set M {(a,b) ∈ c⇧+. a ≠ b} = timpl_closure_set M c"
using timpl_closure'_timpls_trancl_eq'[of c]
timpl_closure_is_timpl_closure'[of _ _ c]
timpl_closure_is_timpl_closure'[of _ _ "{(a,b) ∈ c⇧+. a ≠ b}"]
timpl_closure_set_is_timpl_closure_union[of M c]
timpl_closure_set_is_timpl_closure_union[of M "{(a,b) ∈ c⇧+. a ≠ b}"]
by fastforce
lemma timpl_closure_Var_in_iff:
"Var x ∈ timpl_closure t TI ⟷ t = Var x" (is "?A ⟷ ?B")
proof
have "s ∈ timpl_closure t TI ⟹ s = Var x ⟹ s = t" for s
apply (induction rule: timpl_closure.induct)
by (simp, metis term_variants_pred_inv_Var(2))
thus "?A ⟹ ?B" by blast
qed (blast intro: timpl_closure.FP)
lemma timpl_closure_set_Var_in_iff:
"Var x ∈ timpl_closure_set M TI ⟷ Var x ∈ M"
unfolding timpl_closure_set_def by (simp add: timpl_closure_Var_in_iff[of x _ TI])
lemma timpl_closure_Var_inv:
assumes "t ∈ timpl_closure (Var x) TI"
shows "t = Var x"
using assms
proof (induction rule: timpl_closure.induct)
case (TI u a b s) thus ?case using term_variants_pred_inv_Var by fast
qed simp
lemma timpls_Un_mono: "mono (λX. FP ∪ (⋃x ∈ X. ⋃(a,b) ∈ TI. set ⟨a --» b⟩⟨x⟩))"
by (auto intro!: monoI)
lemma timpl_closure_set_lfp:
fixes M TI
defines "f ≡ λX. M ∪ (⋃x ∈ X. ⋃(a,b) ∈ TI. set ⟨a --» b⟩⟨x⟩)"
shows "lfp f = timpl_closure_set M TI"
proof
note 0 = timpls_Un_mono[of M TI, unfolded f_def[symmetric]]
let ?N = "timpl_closure_set M TI"
show "lfp f ⊆ ?N"
proof (induction rule: lfp_induct)
case 2 thus ?case
proof
fix t assume "t ∈ f (lfp f ∩ ?N)"
hence "t ∈ M ∨ t ∈ (⋃x ∈ ?N. ⋃(a,b) ∈ TI. set ⟨a --» b⟩⟨x⟩)" (is "?A ∨ ?B")
unfolding f_def by blast
thus "t ∈ ?N"
proof
assume ?B
then obtain s a b where s: "s ∈ ?N" "(a,b) ∈ TI" "t ∈ set ⟨a --» b⟩⟨s⟩" by blast
thus ?thesis
using term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])" s]
unfolding timpl_closure_set_def timpl_apply_term_def
by (auto intro: timpl_closure.intros)
qed (auto simp add: timpl_closure_set_def intro: timpl_closure.intros)
qed
qed (rule 0)
have "t ∈ lfp f" when t: "t ∈ timpl_closure s TI" and s: "s ∈ M" for t s
using t
proof (induction t rule: timpl_closure.induct)
case (TI u a b v) thus ?case
using term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
lfp_fixpoint[OF 0]
unfolding timpl_apply_term_def f_def by fastforce
qed (use s lfp_fixpoint[OF 0] f_def in blast)
thus "?N ⊆ lfp f" unfolding timpl_closure_set_def by blast
qed
lemma timpl_closure_set_supset:
assumes "∀t ∈ FP. t ∈ closure"
and "∀t ∈ closure. ∀(a,b) ∈ TI. ∀s ∈ set ⟨a --» b⟩⟨t⟩. s ∈ closure"
shows "timpl_closure_set FP TI ⊆ closure"
proof -
have "t ∈ closure" when t: "t ∈ timpl_closure s TI" and s: "s ∈ FP" for t s
using t
proof (induction rule: timpl_closure.induct)
case FP thus ?case using s assms(1) by blast
next
case (TI u a b s') thus ?case
using assms(2) term_variants_pred_iff_in_term_variants[of "(λ_. [])(Abs a := [Abs b])"]
unfolding timpl_apply_term_def by fastforce
qed
thus ?thesis unfolding timpl_closure_set_def by blast
qed
lemma timpl_closure_set_supset':
assumes "∀t ∈ FP. ∀(a,b) ∈ TI. ∀s ∈ set ⟨a --» b⟩⟨t⟩. s ∈ FP"
shows "timpl_closure_set FP TI ⊆ FP"
using timpl_closure_set_supset[OF _ assms] by blast
lemma timpl_closure'_param:
assumes "(t,s) ∈ timpl_closure' c"
and fg: "f = g ∨ (∃a b. (a,b) ∈ c ∧ f = Abs a ∧ g = Abs b)"
shows "(Fun f (S@t#T), Fun g (S@s#T)) ∈ timpl_closure' c"
using assms(1) unfolding timpl_closure'_def
proof (induction rule: rtrancl_induct)
case base thus ?case
proof (cases "f = g")
case False
then obtain a b where ab: "(a,b) ∈ c" "f = Abs a" "g = Abs b"
using fg by blast
show ?thesis
using term_variants_pred_param[OF term_variants_pred_refl[of "(λ_. [])(Abs a := [Abs b])" t]]
timpl_closure'_step.intros[OF ab(1)] ab(2,3)
by fastforce
qed simp
next
case (step u s)
obtain a b where ab: "(a,b) ∈ c" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u s"
using timpl_closure'_step_inv[OF step.hyps(2)] by blast
have "(Fun g (S@u#T), Fun g (S@s#T)) ∈ timpl_closure'_step c"
using ab(1) term_variants_pred_param[OF ab(2), of g g S T]
by (auto simp add: timpl_closure'_def intro: timpl_closure'_step.intros)
thus ?case using rtrancl_into_rtrancl[OF step.IH] fg by blast
qed
lemma timpl_closure'_param':
assumes "(t,s) ∈ timpl_closure' c"
shows "(Fun f (S@t#T), Fun f (S@s#T)) ∈ timpl_closure' c"
using timpl_closure'_param[OF assms] by simp
lemma timpl_closure_FunI:
assumes IH: "⋀i. i < length T ⟹ (T ! i, S ! i) ∈ timpl_closure' c"
and len: "length T = length S"
and fg: "f = g ∨ (∃a b. (a,b) ∈ c⇧+ ∧ f = Abs a ∧ g = Abs b)"
shows "(Fun f T, Fun g S) ∈ timpl_closure' c"
proof -
have aux: "(Fun f T, Fun g (take n S@drop n T)) ∈ timpl_closure' c"
when "n ≤ length T" for n
using that
proof (induction n)
case 0
have "(T ! n, T ! n) ∈ timpl_closure' c" when n: "n < length T" for n
using n unfolding timpl_closure'_def by simp
hence "(Fun f T, Fun g T) ∈ timpl_closure' c"
proof (cases "f = g")
case False
then obtain a b where ab: "(a, b) ∈ c⇧+" "f = Abs a" "g = Abs b"
using fg by blast
show ?thesis
using timpl_closure'_step.intros[OF ab(1), of "Fun f T" "Fun g T"] ab(2,3)
term_variants_P[OF _ term_variants_pred_refl[of "(λ_. [])(Abs a := [Abs b])"],
of T g f]
timpl_closure'_timpls_trancl_eq
unfolding timpl_closure'_def
by (metis fun_upd_same list.set_intros(1) r_into_rtrancl)
qed (simp add: timpl_closure'_def)
thus ?case by simp
next
case (Suc n)
hence IH': "(Fun f T, Fun g (take n S@drop n T)) ∈ timpl_closure' c"
and n: "n < length T" "n < length S"
by (simp_all add: len)
obtain T1 T2 where T: "T = T1@T ! n#T2" "length T1 = n"
using length_prefix_ex'[OF n(1)] by auto
obtain S1 S2 where S: "S = S1@S ! n#S2" "length S1 = n"
using length_prefix_ex'[OF n(2)] by auto
have "take n S@drop n T = S1@T ! n#T2" "take (Suc n) S@drop (Suc n) T = S1@S ! n#T2"
using n T S append_eq_conv_conj
by (metis, metis (no_types, opaque_lifting) Cons_nth_drop_Suc append.assoc append_Cons
append_Nil take_Suc_conv_app_nth)
moreover have "(T ! n, S ! n) ∈ timpl_closure' c" using IH Suc.prems by simp
ultimately show ?case
using timpl_closure'_param IH'(1)
by (metis (no_types, lifting) timpl_closure'_def rtrancl_trans)
qed
show ?thesis using aux[of "length T"] len by simp
qed
lemma timpl_closure_FunI':
assumes IH: "⋀i. i < length T ⟹ (T ! i, S ! i) ∈ timpl_closure' c"
and len: "length T = length S"
shows "(Fun f T, Fun f S) ∈ timpl_closure' c"
using timpl_closure_FunI[OF IH len] by simp
lemma timpl_closure_FunI2:
fixes f g::"('a, 'b, 'c, 'd) prot_fun"
assumes IH: "⋀i. i < length T ⟹ ∃u. (T!i, u) ∈ timpl_closure' c ∧ (S!i, u) ∈ timpl_closure' c"
and len: "length T = length S"
and fg: "f = g ∨ (∃a b d. (a, d) ∈ c⇧+ ∧ (b, d) ∈ c⇧+ ∧ f = Abs a ∧ g = Abs b)"
shows "∃h U. (Fun f T, Fun h U) ∈ timpl_closure' c ∧ (Fun g S, Fun h U) ∈ timpl_closure' c"
proof -
let ?P = "λi u. (T ! i, u) ∈ timpl_closure' c ∧ (S ! i, u) ∈ timpl_closure' c"
define U where "U ≡ map (λi. SOME u. ?P i u) [0..<length T]"
have U1: "length U = length T"
unfolding U_def by auto
have U2: "(T ! i, U ! i) ∈ timpl_closure' c ∧ (S ! i, U ! i) ∈ timpl_closure' c"
when i: "i < length U" for i
using i someI_ex[of "?P i"] IH[of i] U1 len
unfolding U_def by simp
show ?thesis
proof (cases "f = g")
case False
then obtain a b d where abd: "(a, d) ∈ c⇧+" "(b, d) ∈ c⇧+" "f = Abs a" "g = Abs b"
using fg by blast
define h::"('a, 'b, 'c, 'd) prot_fun" where "h = Abs d"
have "f = h ∨ (∃a b. (a, b) ∈ c⇧+ ∧ f = Abs a ∧ h = Abs b)"
"g = h ∨ (∃a b. (a, b) ∈ c⇧+ ∧ g = Abs a ∧ h = Abs b)"
using abd unfolding h_def by blast+
thus ?thesis by (metis timpl_closure_FunI len U1 U2)
qed (metis timpl_closure_FunI' len U1 U2)
qed
lemma timpl_closure_FunI3:
fixes f g::"('a, 'b, 'c, 'd) prot_fun"
assumes IH: "⋀i. i < length T ⟹ ∃u. (T!i, u) ∈ timpl_closure' c ∧ (S!i, u) ∈ timpl_closure' c"
and len: "length T = length S"
and fg: "f = g ∨ (∃a b d. (a, d) ∈ c ∧ (b, d) ∈ c ∧ f = Abs a ∧ g = Abs b)"
shows "∃h U. (Fun f T, Fun h U) ∈ timpl_closure' c ∧ (Fun g S, Fun h U) ∈ timpl_closure' c"
using timpl_closure_FunI2[OF IH len] fg unfolding timpl_closure'_timpls_trancl_eq by blast
lemma timpl_closure_fv_eq:
assumes "s ∈ timpl_closure t T"
shows "fv s = fv t"
using assms
by (induct rule: timpl_closure.induct)
(metis, metis term_variants_pred_fv_eq)
lemma (in stateful_protocol_model) timpl_closure_subst:
assumes t: "wf⇩t⇩r⇩m t" "∀x ∈ fv t. ∃a. Γ⇩v x = TAtom (Atom a)"
and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)"
shows "timpl_closure (t ⋅ δ) T = timpl_closure t T ⋅⇩s⇩e⇩t δ"
proof
have "s ∈ timpl_closure t T ⋅⇩s⇩e⇩t δ"
when "s ∈ timpl_closure (t ⋅ δ) T" for s
using that
proof (induction s rule: timpl_closure.induct)
case FP thus ?case using timpl_closure.FP[of t T] by simp
next
case (TI u a b s)
then obtain u' where u': "u' ∈ timpl_closure t T" "u = u' ⋅ δ" by blast
have u'_fv: "∀x ∈ fv u'. ∃a. Γ⇩v x = TAtom (Atom a)"
using timpl_closure_fv_eq[OF u'(1)] t(2) by simp
hence u_fv: "∀x ∈ fv u. ∃a. Γ⇩v x = TAtom (Atom a)"
using u'(2) wt_subst_trm''[OF δ(1)] wt_subst_const_fv_type_eq[OF _ δ(1,2), of u']
by fastforce
have "∀x ∈ fv u' ∪ fv s. (∃y. δ x = Var y) ∨ (∃f. δ x = Fun f [] ∧ Abs a ≠ f)"
proof (intro ballI)
fix x assume x: "x ∈ fv u' ∪ fv s"
then obtain c where c: "Γ⇩v x = TAtom (Atom c)"
using u'_fv u_fv term_variants_pred_fv_eq[OF TI.hyps(3)]
by blast
show "(∃y. δ x = Var y) ∨ (∃f. δ x = Fun f [] ∧ Abs a ≠ f)"
proof (cases "δ x")
case (Fun f T)
hence **: "Γ (Fun f T) = TAtom (Atom c)" and "wf⇩t⇩r⇩m (Fun f T)"
using c wt_subst_trm''[OF δ(1), of "Var x"] δ(2)
by fastforce+
hence "δ x = Fun f []" using Fun const_type_inv_wf by metis
thus ?thesis using ** by force
qed metis
qed
hence *: "∀x ∈ fv u' ∪ fv s.
(∃y. δ x = Var y) ∨ (∃f. δ x = Fun f [] ∧ ((λ_. [])(Abs a := [Abs b])) f = [])"
by fastforce
obtain s' where s': "term_variants_pred ((λ_. [])(Abs a := [Abs b])) u' s'" "s = s' ⋅ δ"
using term_variants_pred_subst'[OF _ *] u'(2) TI.hyps(3)
by blast
show ?case using timpl_closure.TI[OF u'(1) TI.hyps(2) s'(1)] s'(2) by blast
qed
thus "timpl_closure (t ⋅ δ) T ⊆ timpl_closure t T ⋅⇩s⇩e⇩t δ" by fast
have "s ∈ timpl_closure (t ⋅ δ) T"
when s: "s ∈ timpl_closure t T ⋅⇩s⇩e⇩t δ" for s
proof -
obtain s' where s': "s' ∈ timpl_closure t T" "s = s' ⋅ δ" using s by blast
have "s' ⋅ δ ∈ timpl_closure (t ⋅ δ) T" using s'(1)
proof (induction s' rule: timpl_closure.induct)
case FP thus ?case using timpl_closure.FP[of "t ⋅ δ" T] by simp
next
case (TI u' a b s') show ?case
using timpl_closure.TI[OF TI.IH TI.hyps(2)]
term_variants_pred_subst[OF TI.hyps(3)]
by blast
qed
thus ?thesis using s'(2) by metis
qed
thus "timpl_closure t T ⋅⇩s⇩e⇩t δ ⊆ timpl_closure (t ⋅ δ) T" by fast
qed
lemma (in stateful_protocol_model) timpl_closure_subst_subset:
assumes t: "t ∈ M"
and M: "wf⇩t⇩r⇩m⇩s M" "∀x ∈ fv⇩s⇩e⇩t M. ∃a. Γ⇩v x = TAtom (Atom a)"
and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)" "ground (subst_range δ)" "subst_domain δ ⊆ fv⇩s⇩e⇩t M"
and M_supset: "timpl_closure t T ⊆ M"
shows "timpl_closure (t ⋅ δ) T ⊆ M ⋅⇩s⇩e⇩t δ"
proof -
have t': "wf⇩t⇩r⇩m t" "∀x ∈ fv t. ∃a. Γ⇩v x = TAtom (Atom a)" using t M by auto
show ?thesis using timpl_closure_subst[OF t' δ(1,2), of T] M_supset by blast
qed
lemma (in stateful_protocol_model) timpl_closure_set_subst_subset:
assumes M: "wf⇩t⇩r⇩m⇩s M" "∀x ∈ fv⇩s⇩e⇩t M. ∃a. Γ⇩v x = TAtom (Atom a)"
and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)" "ground (subst_range δ)" "subst_domain δ ⊆ fv⇩s⇩e⇩t M"
and M_supset: "timpl_closure_set M T ⊆ M"
shows "timpl_closure_set (M ⋅⇩s⇩e⇩t δ) T ⊆ M ⋅⇩s⇩e⇩t δ"
using timpl_closure_subst_subset[OF _ M δ, of _ T] M_supset
timpl_closure_set_is_timpl_closure_union[of "M ⋅⇩s⇩e⇩t δ" T]
timpl_closure_set_is_timpl_closure_union[of M T]
by auto
lemma timpl_closure_set_Union:
"timpl_closure_set (⋃Ms) T = (⋃M ∈ Ms. timpl_closure_set M T)"
using timpl_closure_set_is_timpl_closure_union[of "⋃Ms" T]
timpl_closure_set_is_timpl_closure_union[of _ T]
by force
lemma timpl_closure_set_Union_subst_set:
assumes "s ∈ timpl_closure_set (⋃{M ⋅⇩s⇩e⇩t δ | δ. P δ}) T"
shows "∃δ. P δ ∧ s ∈ timpl_closure_set (M ⋅⇩s⇩e⇩t δ) T"
using assms timpl_closure_set_is_timpl_closure_union[of "(⋃{M ⋅⇩s⇩e⇩t δ | δ. P δ})" T]
timpl_closure_set_is_timpl_closure_union[of _ T]
by blast
lemma timpl_closure_set_Union_subst_singleton:
assumes "s ∈ timpl_closure_set {t ⋅ δ | δ. P δ} T"
shows "∃δ. P δ ∧ s ∈ timpl_closure_set {t ⋅ δ} T"
using assms timpl_closure_set_is_timpl_closure_union[of "{t ⋅ δ |δ. P δ}" T]
timpl_closureton_is_timpl_closure[of _ T]
by fast
lemma timpl_closure'_inv:
assumes "(s, t) ∈ timpl_closure' TI"
shows "(∃x. s = Var x ∧ t = Var x) ∨ (∃f g S T. s = Fun f S ∧ t = Fun g T ∧ length S = length T)"
using assms unfolding timpl_closure'_def
proof (induction rule: rtrancl_induct)
case base thus ?case by (cases s) auto
next
case (step t u)
obtain a b where ab: "(a, b) ∈ TI" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) t u"
using timpl_closure'_step_inv[OF step.hyps(2)] by blast
show ?case using step.IH
proof
assume "∃x. s = Var x ∧ t = Var x"
thus ?case using step.hyps(2) term_variants_pred_inv_Var ab by fastforce
next
assume "∃f g S T. s = Fun f S ∧ t = Fun g T ∧ length S = length T"
then obtain f g S T where st: "s = Fun f S" "t = Fun g T" "length S = length T" by blast
thus ?case
using ab step.hyps(2) term_variants_pred_inv'[of "(λ_. [])(Abs a := [Abs b])" g T u]
by auto
qed
qed
lemma timpl_closure'_inv':
assumes "(s, t) ∈ timpl_closure' TI"
shows "(∃x. s = Var x ∧ t = Var x) ∨
(∃f g S T. s = Fun f S ∧ t = Fun g T ∧ length S = length T ∧
(∀i < length T. (S ! i, T ! i) ∈ timpl_closure' TI) ∧
(f ≠ g ⟶ is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ TI⇧+))"
(is "?A s t ∨ ?B s t (timpl_closure' TI)")
using assms unfolding timpl_closure'_def
proof (induction rule: rtrancl_induct)
case base thus ?case by (cases s) auto
next
case (step t u)
obtain a b where ab: "(a, b) ∈ TI" "term_variants_pred ((λ_. [])(Abs a := [Abs b])) t u"
using timpl_closure'_step_inv[OF step.hyps(2)] by blast
show ?case using step.IH
proof
assume "?A s t"
thus ?case using step.hyps(2) term_variants_pred_inv_Var ab by fastforce
next
assume "?B s t ((timpl_closure'_step TI)⇧*)"
then obtain f g S T where st:
"s = Fun f S" "t = Fun g T" "length S = length T"
"⋀i. i < length T ⟹ (S ! i, T ! i) ∈ (timpl_closure'_step TI)⇧*"
"f ≠ g ⟹ is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ TI⇧+"
by blast
obtain h U where u:
"u = Fun h U" "length T = length U"
"⋀i. i < length T ⟹ term_variants_pred ((λ_. [])(Abs a := [Abs b])) (T ! i) (U ! i)"
"g ≠ h ⟹ is_Abs g ∧ is_Abs h ∧ (the_Abs g, the_Abs h) ∈ TI⇧+"
using ab(2) st(2) r_into_trancl[OF ab(1)]
term_variants_pred_inv'(1,2,3,4)[of "(λ_. [])(Abs a := [Abs b])" g T u]
term_variants_pred_inv'(5)[of "(λ_. [])(Abs a := [Abs b])" g T u "Abs a" "Abs b"]
unfolding is_Abs_def the_Abs_def by force
have "(S ! i, U ! i) ∈ (timpl_closure'_step TI)⇧*" when i: "i < length U" for i
using u(2) i rtrancl.rtrancl_into_rtrancl[OF
st(4)[of i] timpl_closure'_step.intros[OF ab(1) u(3)[of i]]]
by argo
moreover have "length S = length U" using st u by argo
moreover have "is_Abs f ∧ is_Abs h ∧ (the_Abs f, the_Abs h) ∈ TI⇧+" when fh: "f ≠ h"
using fh st u by fastforce
ultimately show ?case using st(1) u(1) by blast
qed
qed
lemma timpl_closure'_inv'':
assumes "(Fun f S, Fun g T) ∈ timpl_closure' TI"
shows "length S = length T"
and "⋀i. i < length T ⟹ (S ! i, T ! i) ∈ timpl_closure' TI"
and "f ≠ g ⟹ is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ TI⇧+"
using assms timpl_closure'_inv' by auto
lemma timpl_closure_Fun_inv:
assumes "s ∈ timpl_closure (Fun f T) TI"
shows "∃g S. s = Fun g S"
using assms timpl_closure_is_timpl_closure' timpl_closure'_inv
by fastforce
lemma timpl_closure_Fun_inv':
assumes "Fun g S ∈ timpl_closure (Fun f T) TI"
shows "length S = length T"
and "⋀i. i < length S ⟹ S ! i ∈ timpl_closure (T ! i) TI"
and "f ≠ g ⟹ is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ TI⇧+"
using assms timpl_closure_is_timpl_closure'
by (metis timpl_closure'_inv''(1), metis timpl_closure'_inv''(2), metis timpl_closure'_inv''(3))
lemma timpl_closure_Fun_not_Var[simp]:
"Fun f T ∉ timpl_closure (Var x) TI"
using timpl_closure_Var_inv by fast
lemma timpl_closure_Var_not_Fun[simp]:
"Var x ∉ timpl_closure (Fun f T) TI"
using timpl_closure_Fun_inv by fast
lemma (in stateful_protocol_model) timpl_closure_wf_trms:
assumes m: "wf⇩t⇩r⇩m m"
shows "wf⇩t⇩r⇩m⇩s (timpl_closure m TI)"
proof
fix t assume "t ∈ timpl_closure m TI"
thus "wf⇩t⇩r⇩m t"
proof (induction t rule: timpl_closure.induct)
case TI thus ?case using term_variants_pred_wf_trms by force
qed (rule m)
qed
lemma (in stateful_protocol_model) timpl_closure_set_wf_trms:
assumes M: "wf⇩t⇩r⇩m⇩s M"
shows "wf⇩t⇩r⇩m⇩s (timpl_closure_set M TI)"
proof
fix t assume "t ∈ timpl_closure_set M TI"
then obtain m where "t ∈ timpl_closure m TI" "m ∈ M" "wf⇩t⇩r⇩m m"
using M timpl_closure_set_is_timpl_closure_union by blast
thus "wf⇩t⇩r⇩m t" using timpl_closure_wf_trms by blast
qed
lemma timpl_closure_Fu_inv:
assumes "t ∈ timpl_closure (Fun (Fu f) T) TI"
shows "∃S. length S = length T ∧ t = Fun (Fu f) S"
using assms
proof (induction t rule: timpl_closure.induct)
case (TI u a b s)
then obtain U where U: "length U = length T" "u = Fun (Fu f) U"
by blast
hence *: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) (Fun (Fu f) U) s"
using TI.hyps(3) by meson
show ?case
using term_variants_pred_inv'(1,2,4)[OF *] U
by force
qed simp
lemma timpl_closure_Fu_inv':
assumes "Fun (Fu f) T ∈ timpl_closure t TI"
shows "∃S. length S = length T ∧ t = Fun (Fu f) S"
using assms
proof (induction "Fun (Fu f) T" arbitrary: T rule: timpl_closure.induct)
case (TI u a b)
obtain g U where U:
"u = Fun g U" "length U = length T"
"Fu f ≠ g ⟹ Abs a = g ∧ Fu f = Abs b"
using term_variants_pred_inv''[OF TI.hyps(4)] by fastforce
have g: "g = Fu f" using U(3) by blast
show ?case using TI.hyps(2)[OF U(1)[unfolded g]] U(2) by auto
qed simp
lemma timpl_closure_no_Abs_eq:
assumes "t ∈ timpl_closure s TI"
and "∀f ∈ funs_term t. ¬is_Abs f"
shows "t = s"
using assms
proof (induction t rule: timpl_closure.induct)
case (TI t a b s) thus ?case
using term_variants_pred_eq_case_Abs[of a b t s]
unfolding timpl_apply_term_def term_variants_pred_iff_in_term_variants[symmetric]
by metis
qed simp
lemma timpl_closure_set_no_Abs_in_set:
assumes "t ∈ timpl_closure_set FP TI"
and "∀f ∈ funs_term t. ¬is_Abs f"
shows "t ∈ FP"
using assms timpl_closure_no_Abs_eq unfolding timpl_closure_set_def by blast
lemma timpl_closure_funs_term_subset:
"⋃(funs_term ` (timpl_closure t TI)) ⊆ funs_term t ∪ Abs ` snd ` TI"
(is "?A ⊆ ?B ∪ ?C")
proof
fix f assume "f ∈ ?A"
then obtain s where "s ∈ timpl_closure t TI" "f ∈ funs_term s" by blast
thus "f ∈ ?B ∪ ?C"
proof (induction s rule: timpl_closure.induct)
case (TI u a b s)
have "Abs b ∈ Abs ` snd ` TI" using TI.hyps(2) by force
thus ?case using term_variants_pred_funs_term[OF TI.hyps(3) TI.prems] TI.IH by force
qed blast
qed
lemma timpl_closure_set_funs_term_subset:
"⋃(funs_term ` (timpl_closure_set FP TI)) ⊆ ⋃(funs_term ` FP) ∪ Abs ` snd ` TI"
using timpl_closure_funs_term_subset[of _ TI]
timpl_closure_set_is_timpl_closure_union[of FP TI]
by auto
lemma funs_term_OCC_TI_subset:
defines "absc ≡ λa. Fun (Abs a) []"
assumes OCC1: "∀t ∈ FP. ∀f ∈ funs_term t. is_Abs f ⟶ f ∈ Abs ` OCC"
and OCC2: "snd ` TI ⊆ OCC"
shows "∀t ∈ timpl_closure_set FP TI. ∀f ∈ funs_term t. is_Abs f ⟶ f ∈ Abs ` OCC" (is ?A)
and "∀t ∈ absc ` OCC. ∀(a,b) ∈ TI. ∀s ∈ set ⟨a --» b⟩⟨t⟩. s ∈ absc ` OCC" (is ?B)
proof -
let ?F = "⋃(funs_term ` FP)"
let ?G = "Abs ` snd ` TI"
show ?A
proof (intro ballI impI)
fix t f assume t: "t ∈ timpl_closure_set FP TI" and f: "f ∈ funs_term t" "is_Abs f"
hence "f ∈ ?F ∨ f ∈ ?G" using timpl_closure_set_funs_term_subset[of FP TI] by auto
thus "f ∈ Abs ` OCC"
proof
assume "f ∈ ?F" thus ?thesis using OCC1 f(2) by fast
next
assume "f ∈ ?G" thus ?thesis using OCC2 by auto
qed
qed
{ fix s t a b
assume t: "t ∈ absc ` OCC"
and ab: "(a, b) ∈ TI"
and s: "s ∈ set ⟨a --» b⟩⟨t⟩"
obtain c where c: "t = absc c" "c ∈ OCC" using t by blast
hence "s = absc b ∨ s = absc c"
using ab s timpl_apply_const'[of c a b] unfolding absc_def by auto
moreover have "b ∈ OCC" using ab OCC2 by auto
ultimately have "s ∈ absc ` OCC" using c(2) by blast
} thus ?B by blast
qed
lemma (in stateful_protocol_model) intruder_synth_timpl_closure_set:
fixes M::"('fun,'atom,'sets,'lbl) prot_terms" and t::"('fun,'atom,'sets,'lbl) prot_term"
assumes "M ⊢⇩c t"
and "s ∈ timpl_closure t TI"
shows "timpl_closure_set M TI ⊢⇩c s"
using assms
proof (induction t arbitrary: s rule: intruder_synth_induct)
case (AxiomC t)
hence "s ∈ timpl_closure_set M TI"
using timpl_closure_set_is_timpl_closure_union[of M TI]
by blast
thus ?case by simp
next
case (ComposeC T f)
obtain g S where s: "s = Fun g S"
using timpl_closure_Fun_inv[OF ComposeC.prems] by blast
hence s':
"f = g" "length S = length T"
"⋀i. i < length S ⟹ S ! i ∈ timpl_closure (T ! i) TI"
using timpl_closure_Fun_inv'[of g S f T TI] ComposeC.prems ComposeC.hyps(2)
unfolding is_Abs_def by fastforce+
have "timpl_closure_set M TI ⊢⇩c u" when u: "u ∈ set S" for u
using ComposeC.IH u s'(2,3) in_set_conv_nth[of _ T] in_set_conv_nth[of u S] by auto
thus ?case
using s s'(1,2) ComposeC.hyps(1,2) intruder_synth.ComposeC[of S g "timpl_closure_set M TI"]
by argo
qed
lemma (in stateful_protocol_model) intruder_synth_timpl_closure':
fixes M::"('fun,'atom,'sets,'lbl) prot_terms" and t::"('fun,'atom,'sets,'lbl) prot_term"
assumes "timpl_closure_set M TI ⊢⇩c t"
and "s ∈ timpl_closure t TI"
shows "timpl_closure_set M TI ⊢⇩c s"
by (metis intruder_synth_timpl_closure_set[OF assms] timpl_closure_set_idem)
lemma timpl_closure_set_absc_subset_in:
defines "absc ≡ λa. Fun (Abs a) []"
assumes A: "timpl_closure_set (absc ` A) TI ⊆ absc ` A"
and a: "a ∈ A" "(a,b) ∈ TI⇧+"
shows "b ∈ A"
proof -
have "timpl_closure (absc a) (TI⇧+) ⊆ absc ` A"
using a(1) A timpl_closure_timpls_trancl_eq
unfolding timpl_closure_set_def by fast
thus ?thesis
using timpl_closure.TI[OF timpl_closure.FP[of "absc a"] a(2), of "absc b"]
term_variants_P[of "[]" "[]" "(λ_. [])(Abs a := [Abs b])" "Abs b" "Abs a"]
unfolding absc_def by auto
qed
lemma timpl_closure_Abs_ex:
assumes t: "s ∈ timpl_closure t TI"
and a: "Abs a ∈ funs_term t"
shows "∃b ts. (a,b) ∈ TI⇧* ∧ Fun (Abs b) ts ⊑ s"
using t
proof (induction rule: timpl_closure.induct)
case (TI u b c s)
obtain d ts where d: "(a,d) ∈ TI⇧*" "Fun (Abs d) ts ⊑ u" using TI.IH by blast
note 0 = TI.hyps(2) d(1) term_variants_pred_inv'(5)[OF term_variants_pred_const]
show ?case using TI.hyps(3) d(2)
proof (induction rule: term_variants_pred.induct)
case (term_variants_P T S g f)
note hyps = term_variants_P.hyps
note prems = term_variants_P.prems
note IH = term_variants_P.IH
show ?case
proof (cases "Fun (Abs d) ts = Fun f T")
case False
hence "∃t ∈ set T. Fun (Abs d) ts ⊑ t" using prems(1) by force
then obtain i where i: "i < length T" "Fun (Abs d) ts ⊑ T ! i" by (metis in_set_conv_nth)
show ?thesis by (metis IH[OF i] i(1) hyps(1) nth_mem subtermeqI'' term.order.trans)
qed (metis hyps(3) 0 prot_fun.sel(4) r_into_rtrancl rtrancl_trans term.eq_refl term.sel(2))
next
case (term_variants_Fun T S f)
note hyps = term_variants_Fun.hyps
note prems = term_variants_Fun.prems
note IH = term_variants_Fun.IH
show ?case
proof (cases "Fun (Abs d) ts = Fun f T")
case False
hence "∃t ∈ set T. Fun (Abs d) ts ⊑ t" using prems(1) by force
then obtain i where i: "i < length T" "Fun (Abs d) ts ⊑ T ! i" by (metis in_set_conv_nth)
show ?thesis by (metis IH[OF i] i(1) hyps(1) nth_mem subtermeqI'' term.order.trans)
qed (metis 0(2) term.eq_refl term.sel(2))
qed simp
qed (meson a funs_term_Fun_subterm rtrancl_eq_or_trancl)
lemma timpl_closure_trans:
assumes "s ∈ timpl_closure t TI"
and "u ∈ timpl_closure s TI"
shows "u ∈ timpl_closure t TI"
using assms unfolding timpl_closure_is_timpl_closure' timpl_closure'_def by simp
lemma (in stateful_protocol_model) term_variants_pred_Ana⇩f_keys:
assumes
"length ss = length ts"
"∀x ∈ fv k. x < length ss"
"⋀i. i < length ss ⟹ term_variants_pred P (ss ! i) (ts ! i)"
shows "term_variants_pred P (k ⋅ (!) ss) (k ⋅ (!) ts)"
using assms by (meson term_variants_pred_subst'')
lemma (in stateful_protocol_model) term_variants_pred_Ana_keys:
fixes a b and s t::"('fun,'atom,'sets,'lbl) prot_term"
defines "P ≡ ((λ_. [])(Abs a := [Abs b]))"
assumes ab: "term_variants_pred P s t"
and s: "Ana s = (Ks, Rs)"
and t: "Ana t = (Kt, Rt)"
shows "length Kt = length Ks" (is ?A)
and "∀i < length Ks. term_variants_pred P (Ks ! i) (Kt ! i)" (is ?B)
proof -
have ?A ?B when "s = Var x" for x
using that ab s t iffD1[OF term_variants_pred_inv_Var(1) ab[unfolded that]] by auto
moreover have ?A ?B when s': "s = Fun f ss" for f ss
proof -
obtain g ts where t':
"t = Fun g ts" "length ss = length ts"
"⋀i. i < length ss ⟹ term_variants_pred P (ss ! i) (ts ! i)"
"f ≠ g ⟹ f = Abs a ∧ g = Abs b"
using term_variants_pred_inv'[OF ab[unfolded s']]
unfolding P_def by fastforce
have ?A ?B when "f ≠ g" using that s s' t t'(1,2,4) by auto
moreover have A: ?A when fg: "f = g"
using s t Ana_Fu_keys_length_eq[OF t'(2)] Ana_nonempty_inv[of s] Ana_nonempty_inv[of t]
unfolding fg s' t'(1) by (metis (no_types) fst_conv term.inject(2))
moreover have ?B when fg: "f = g"
proof (cases "Ana s = ([],[])")
case True thus ?thesis using s t t'(2,3) A[OF fg] unfolding fg s' t'(1) by auto
next
case False
then obtain h Kh Rh where h:
"f = Fu h" "g = Fu h" "arity⇩f h = length ss" "arity⇩f h > 0" "Ana⇩f h = (Kh, Rh)"
"Ana s = (Kh ⋅⇩l⇩i⇩s⇩t (!) ss, map ((!) ss) Rh)" "Ana t = (Kh ⋅⇩l⇩i⇩s⇩t (!) ts, map ((!) ts) Rh)"
using A[OF fg] s t t'(2,3) Ana_nonempty_inv[of s] Ana_nonempty_inv[of t]
unfolding fg s' t'(1) by fastforce
show ?thesis
proof (intro allI impI)
fix i assume i: "i < length Ks"
have Ks: "Ks = Kh ⋅⇩l⇩i⇩s⇩t (!) ss" and Kt: "Kt = Kh ⋅⇩l⇩i⇩s⇩t (!) ts"
using h(6,7) s t by auto
have 0: "Kh ! i ∈ set Kh" using Ks i by simp
have 1: "∀x ∈ fv (Kh ! i). x < length ss"
using 0 Ana⇩f_assm2_alt[OF h(5)]
unfolding h(1-3) by fastforce
have "term_variants_pred P (Kh ! i ⋅ (!) ss) (Kh ! i ⋅ (!) ts)"
using term_variants_pred_Ana⇩f_keys[OF t'(2) 1 t'(3)]
unfolding P_def by fast
thus "term_variants_pred P (Ks ! i) (Kt ! i)"
using i unfolding Ks Kt by simp
qed
qed
ultimately show ?A ?B by fast+
qed
ultimately show ?A ?B by (cases s; simp_all)+
qed
lemma (in stateful_protocol_model) timpl_closure_Ana_keys:
fixes s t::"('fun,'atom,'sets,'lbl) prot_term"
assumes "t ∈ timpl_closure s TI"
and "Ana s = (Ks, Rs)"
and "Ana t = (Kt, Rt)"
shows "length Kt = length Ks" (is ?A)
and "∀i < length Ks. Kt ! i ∈ timpl_closure (Ks ! i) TI" (is ?B)
using assms
proof (induction arbitrary: Ks Rs Kt Rt rule: timpl_closure.induct)
case FP
{ case 1 thus ?case by simp }
{ case 2 thus ?case using FP timpl_closure.FP by force }
next
case (TI u a b t)
obtain Ku Ru where u: "Ana u = (Ku, Ru)" by (metis surj_pair)
note 0 = term_variants_pred_Ana_keys[OF TI.hyps(3) u]
{ case 1 thus ?case using 0(1) TI.IH(1) u by fastforce }
{ case 2 thus ?case by (metis 0(2)[OF 2(2)] TI.IH[OF 2(1) u] timpl_closure.TI[OF _ TI.hyps(2)]) }
qed
lemma (in stateful_protocol_model) timpl_closure_Ana_keys_length_eq:
fixes s t::"('fun,'atom,'sets,'lbl) prot_term"
assumes "t ∈ timpl_closure s TI"
and "Ana s = (Ks, Rs)"
and "Ana t = (Kt, Rt)"
shows "length Kt = length Ks"
by (rule timpl_closure_Ana_keys(1,2)[OF assms])
lemma (in stateful_protocol_model) timpl_closure_Ana_keys_subset:
fixes s t::"('fun,'atom,'sets,'lbl) prot_term"
assumes "t ∈ timpl_closure s TI"
and "Ana s = (Ks, Rs)"
and "Ana t = (Kt, Rt)"
shows "set Kt ⊆ timpl_closure_set (set Ks) TI"
proof -
note 0 = timpl_closure_Ana_keys[OF assms]
have "∀i < length Ks. Kt ! i ∈ timpl_closure_set (set Ks) TI"
using in_set_conv_nth 0(2) unfolding timpl_closure_set_def by auto
thus "set Kt ⊆ timpl_closure_set (set Ks) TI"
using 0(1) by (metis subsetI in_set_conv_nth)
qed
subsection ‹Composition-only Intruder Deduction Modulo Term Implication Closure of the Intruder Knowledge›
context stateful_protocol_model
begin
fun in_trancl where
"in_trancl TI a b = (
if (a,b) ∈ set TI then True
else list_ex (λ(c,d). c = a ∧ in_trancl (removeAll (c,d) TI) d b) TI)"
definition in_rtrancl where
"in_rtrancl TI a b ≡ a = b ∨ in_trancl TI a b"
declare in_trancl.simps[simp del]
fun timpls_transformable_to where
"timpls_transformable_to TI (Var x) (Var y) = (x = y)"
| "timpls_transformable_to TI (Fun f T) (Fun g S) = (
(f = g ∨ (is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ set TI)) ∧
list_all2 (timpls_transformable_to TI) T S)"
| "timpls_transformable_to _ _ _ = False"
fun timpls_transformable_to' where
"timpls_transformable_to' TI (Var x) (Var y) = (x = y)"
| "timpls_transformable_to' TI (Fun f T) (Fun g S) = (
(f = g ∨ (is_Abs f ∧ is_Abs g ∧ in_trancl TI (the_Abs f) (the_Abs g))) ∧
list_all2 (timpls_transformable_to' TI) T S)"
| "timpls_transformable_to' _ _ _ = False"
fun equal_mod_timpls where
"equal_mod_timpls TI (Var x) (Var y) = (x = y)"
| "equal_mod_timpls TI (Fun f T) (Fun g S) = (
(f = g ∨ (is_Abs f ∧ is_Abs g ∧
((the_Abs f, the_Abs g) ∈ set TI ∨
(the_Abs g, the_Abs f) ∈ set TI ∨
(∃ti ∈ set TI. (the_Abs f, snd ti) ∈ set TI ∧ (the_Abs g, snd ti) ∈ set TI)))) ∧
list_all2 (equal_mod_timpls TI) T S)"
| "equal_mod_timpls _ _ _ = False"
fun intruder_synth_mod_timpls where
"intruder_synth_mod_timpls M TI (Var x) = List.member M (Var x)"
| "intruder_synth_mod_timpls M TI (Fun f T) = (
(list_ex (λt. timpls_transformable_to TI t (Fun f T)) M) ∨
(public f ∧ length T = arity f ∧ list_all (intruder_synth_mod_timpls M TI) T))"
fun intruder_synth_mod_timpls' where
"intruder_synth_mod_timpls' M TI (Var x) = List.member M (Var x)"
| "intruder_synth_mod_timpls' M TI (Fun f T) = (
(list_ex (λt. timpls_transformable_to' TI t (Fun f T)) M) ∨
(public f ∧ length T = arity f ∧ list_all (intruder_synth_mod_timpls' M TI) T))"
fun intruder_synth_mod_eq_timpls where
"intruder_synth_mod_eq_timpls M TI (Var x) = (Var x ∈ M)"
| "intruder_synth_mod_eq_timpls M TI (Fun f T) = (
(∃t ∈ M. equal_mod_timpls TI t (Fun f T)) ∨
(public f ∧ length T = arity f ∧ list_all (intruder_synth_mod_eq_timpls M TI) T))"
definition analyzed_closed_mod_timpls where
"analyzed_closed_mod_timpls M TI ≡
let ti = intruder_synth_mod_timpls M TI;
cl = λts. comp_timpl_closure ts (set TI);
f = list_all ti;
g = λt. if f (fst (Ana t)) then f (snd (Ana t))
else if list_all (λt. ∀f ∈ funs_term t. ¬is_Abs f) (fst (Ana t)) then True
else if ∀s ∈ cl (set (fst (Ana t))). ¬ti s then True
else ∀s ∈ cl {t}. case Ana s of (K,R) ⇒ f K ⟶ f R
in list_all g M"
definition analyzed_closed_mod_timpls' where
"analyzed_closed_mod_timpls' M TI ≡
let f = list_all (intruder_synth_mod_timpls' M TI);
g = λt. if f (fst (Ana t)) then f (snd (Ana t))
else if list_all (λt. ∀f ∈ funs_term t. ¬is_Abs f) (fst (Ana t)) then True
else ∀s ∈ comp_timpl_closure {t} (set TI). case Ana s of (K,R) ⇒ f K ⟶ f R
in list_all g M"
lemma term_variants_pred_Abs_Ana_keys:
fixes a b
defines "P ≡ ((λ_. [])(Abs a := [Abs b]))"
assumes st: "term_variants_pred P s t"
shows "length (fst (Ana s)) = length (fst (Ana t))" (is "?P s t")
and "∀i < length (fst (Ana s)). term_variants_pred P (fst (Ana s) ! i) (fst (Ana t) ! i)"
(is "?Q s t")
proof -
show "?P s t" using st
proof (induction s t rule: term_variants_pred.induct)
case (term_variants_Fun T S f) show ?case
proof (cases f)
case (Fu g) thus ?thesis using term_variants_Fun Ana_Fu_keys_length_eq by blast
qed simp_all
qed (simp_all add: P_def)
show "?Q s t" using st
proof (induction s t rule: term_variants_pred.induct)
case (term_variants_Fun T S f)
note hyps = term_variants_Fun.hyps
let ?K = "λU. fst (Ana (Fun f U))"
show ?case
proof (cases f)
case (Fu g) show ?thesis
proof (cases "arity⇩f g = length T ∧ arity⇩f g > 0")
case True
hence *: "?K T = fst (Ana⇩f g) ⋅⇩l⇩i⇩s⇩t (!) T"
"?K S = fst (Ana⇩f g) ⋅⇩l⇩i⇩s⇩t (!) S"
using Fu Ana_Fu_intro fst_conv prod.collapse
by (metis (mono_tags, lifting), metis (mono_tags, lifting) hyps(1))
have K: "j < length T" when j: "j ∈ fv⇩s⇩e⇩t (set (fst (Ana⇩f g)))" for j
using True Ana⇩f_assm2_alt[of g "fst (Ana⇩f g)" _ j ]
by (metis UnI1 prod.collapse that)
show ?thesis
proof (intro allI impI)
fix i assume i: "i < length (?K T)"
let ?u = "fst (Ana⇩f g) ! i"
have **: "?K T ! i = ?u ⋅ (!) T" "?K S ! i = ?u ⋅ (!) S"
using * i by simp_all
have ***: "x < length T" when "x ∈ fv (fst (Ana⇩f g) ! i)" for x
using that K Ana⇩f_assm2_alt[of g "fst (Ana⇩f g)" _ x] i hyps(1)
unfolding * by force
show "term_variants_pred P (?K T ! i) (?K S ! i)"
using i hyps K *** term_variants_pred_subst''[of ?u P "(!) T" "(!) S"]
unfolding * by auto
qed
qed (auto simp add: Fu)
qed simp_all
qed (simp_all add: P_def)
qed
lemma term_variants_pred_Abs_eq_case:
assumes t: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) s t" (is "?R s t")
and s: "∀f ∈ funs_term s. ¬is_Abs f" (is "?P s")
shows "s = t"
using s term_variants_pred_eq_case[OF t] by fastforce
lemma term_variants_Ana_keys_no_Abs_eq_case:
fixes s t::"(('fun,'atom,'sets,'lbl) prot_fun,'v) term"
assumes t: "term_variants_pred ((λ_. [])(Abs a := [Abs b])) s t" (is "?R s t")
and s: "∀t ∈ set (fst (Ana s)). ∀f ∈ funs_term t. ¬is_Abs f" (is "?P s")
shows "fst (Ana t) = fst (Ana s)" (is "?Q t s")
using s term_variants_pred_Abs_Ana_keys[OF t] term_variants_pred_Abs_eq_case[of a b]
by (metis nth_equalityI nth_mem)
lemma timpl_closure_Ana_keys_no_Abs_eq_case:
assumes t: "t ∈ timpl_closure s TI"
and s: "∀t ∈ set (fst (Ana s)). ∀f ∈ funs_term t. ¬is_Abs f" (is "?P s")
shows "fst (Ana t) = fst (Ana s)"
using t
proof (induction t rule: timpl_closure.induct)
case (TI u a b t)
thus ?case using s term_variants_Ana_keys_no_Abs_eq_case by fastforce
qed simp
lemma in_trancl_closure_iff_in_trancl_fun:
"(a,b) ∈ (set TI)⇧+ ⟷ in_trancl TI a b" (is "?A TI a b ⟷ ?B TI a b")
proof
show "?A TI a b ⟹ ?B TI a b"
proof (induction rule: trancl_induct)
case (step c d)
show ?case using step.IH step.hyps(2)
proof (induction TI a c rule: in_trancl.induct)
case (1 TI a b)
have "(a,b) ∈ set TI ∨ (∃e. (a,e) ∈ set TI ∧ in_trancl (removeAll (a,e) TI) e b)"
using "1.prems"(1) in_trancl.simps[of TI a b]
unfolding list_ex_iff by (cases "(a,b) ∈ set TI") auto
show ?case
proof (cases "(a,b) ∈ set TI")
case True thus ?thesis
by (metis (mono_tags, lifting) in_trancl.simps "1.prems"(2) list_ex_iff case_prodI
member_remove prod.inject remove_code(1))
next
case F: False
then obtain e where e: "(a,e) ∈ set TI" "in_trancl (removeAll (a,e) TI) e b"
using "1.prems"(1) in_trancl.simps[of TI a b]
unfolding list_ex_iff by (cases "(a,b) ∈ set TI") auto
show ?thesis
proof (cases "(b, d) ∈ set (removeAll (a, e) TI)")
case True thus ?thesis
using in_trancl.simps[of TI a d] e(1) "1.prems"(2) "1.IH"[OF F e(1) _ e(2)]
unfolding list_ex_iff by auto
next
case False thus ?thesis using in_trancl.simps[of TI a d] "1.prems"(2) by simp
qed
qed
qed
qed (metis in_trancl.simps)
show "?B TI a b ⟹ ?A TI a b"
proof (induction TI a b rule: in_trancl.induct)
case (1 TI a b)
let ?P = "λTI a b c d. in_trancl (List.removeAll (c,d) TI) d b"
have *: "∃(c,d) ∈ set TI. c = a ∧ ?P TI a b c d" when "(a,b) ∉ set TI"
using that "1.prems" list_ex_iff[of _ TI] in_trancl.simps[of TI a b]
by auto
show ?case
proof (cases "(a,b) ∈ set TI")
case False
hence "∃(c,d) ∈ set TI. c = a ∧ ?P TI a b c d" using * by blast
then obtain d where d: "(a,d) ∈ set TI" "?P TI a b a d" by blast
have "(d,b) ∈ (set (removeAll (a,d) TI))⇧+" using "1.IH"[OF False d(1)] d(2) by blast
moreover have "set (removeAll (a,d) TI) ⊆ set TI" by simp
ultimately have "(d,b) ∈ (set TI)⇧+" using trancl_mono by blast
thus ?thesis using d(1) by fastforce
qed simp
qed
qed
lemma in_rtrancl_closure_iff_in_rtrancl_fun:
"(a,b) ∈ (set TI)⇧* ⟷ in_rtrancl TI a b"
by (metis rtrancl_eq_or_trancl in_trancl_closure_iff_in_trancl_fun in_rtrancl_def)
lemma in_trancl_mono:
assumes "set TI ⊆ set TI'"
and "in_trancl TI a b"
shows "in_trancl TI' a b"
by (metis assms in_trancl_closure_iff_in_trancl_fun trancl_mono)
lemma equal_mod_timpls_refl:
"equal_mod_timpls TI t t"
proof (induction t)
case (Fun f T) thus ?case
using list_all2_conv_all_nth[of "equal_mod_timpls TI" T T] by force
qed simp
lemma equal_mod_timpls_inv_Var:
"equal_mod_timpls TI (Var x) t ⟹ t = Var x" (is "?A ⟹ ?C")
"equal_mod_timpls TI t (Var x) ⟹ t = Var x" (is "?B ⟹ ?C")
proof -
show "?A ⟹ ?C" by (cases t) auto
show "?B ⟹ ?C" by (cases t) auto
qed
lemma equal_mod_timpls_inv:
assumes "equal_mod_timpls TI (Fun f T) (Fun g S)"
shows "length T = length S"
and "⋀i. i < length T ⟹ equal_mod_timpls TI (T ! i) (S ! i)"
and "f ≠ g ⟹ (is_Abs f ∧ is_Abs g ∧ (
(the_Abs f, the_Abs g) ∈ set TI ∨ (the_Abs g, the_Abs f) ∈ set TI ∨
(∃ti ∈ set TI. (the_Abs f, snd ti) ∈ set TI ∧
(the_Abs g, snd ti) ∈ set TI)))"
using assms list_all2_conv_all_nth[of "equal_mod_timpls TI" T S]
by (auto elim: equal_mod_timpls.cases)
lemma equal_mod_timpls_inv':
assumes "equal_mod_timpls TI (Fun f T) t"
shows "is_Fun t"
and "length T = length (args t)"
and "⋀i. i < length T ⟹ equal_mod_timpls TI (T ! i) (args t ! i)"
and "f ≠ the_Fun t ⟹ (is_Abs f ∧ is_Abs (the_Fun t) ∧ (
(the_Abs f, the_Abs (the_Fun t)) ∈ set TI ∨
(the_Abs (the_Fun t), the_Abs f) ∈ set TI ∨
(∃ti ∈ set TI. (the_Abs f, snd ti) ∈ set TI ∧
(the_Abs (the_Fun t), snd ti) ∈ set TI)))"
and "¬is_Abs f ⟹ f = the_Fun t"
using assms list_all2_conv_all_nth[of "equal_mod_timpls TI" T]
by (cases t; auto)+
lemma equal_mod_timpls_if_term_variants:
fixes s t::"(('a, 'b, 'c, 'd) prot_fun, 'e) term" and a b::"'c set"
defines "P ≡ (λ_. [])(Abs a := [Abs b])"
assumes st: "term_variants_pred P s t"
and ab: "(a,b) ∈ set TI"
shows "equal_mod_timpls TI s t"
using st P_def
proof (induction rule: term_variants_pred.induct)
case (term_variants_P T S f) thus ?case
using ab list_all2_conv_all_nth[of "equal_mod_timpls TI" T S]
in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
by auto
next
case (term_variants_Fun T S f) thus ?case
using ab list_all2_conv_all_nth[of "equal_mod_timpls TI" T S]
in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
by auto
qed simp
lemma equal_mod_timpls_mono:
assumes "set TI ⊆ set TI'"
and "equal_mod_timpls TI s t"
shows "equal_mod_timpls TI' s t"
using assms
proof (induction TI s t rule: equal_mod_timpls.induct)
case (2 TI f T g S)
have *: "f = g ∨ (is_Abs f ∧ is_Abs g ∧ ((the_Abs f, the_Abs g) ∈ set TI ∨
(the_Abs g, the_Abs f) ∈ set TI ∨
(∃ti ∈ set TI. (the_Abs f, snd ti) ∈ set TI ∧
(the_Abs g, snd ti) ∈ set TI)))"
"list_all2 (equal_mod_timpls TI) T S"
using "2.prems" by simp_all
show ?case
using "2.IH"[OF _ _ "2.prems"(1)] list.rel_mono_strong[OF *(2), of "equal_mod_timpls TI'"]
*(1) in_trancl_mono[OF "2.prems"(1)] set_rev_mp[OF _ "2.prems"(1)]
equal_mod_timpls.simps(2)[of TI' f T g S]
by metis
qed auto
lemma equal_mod_timpls_refl_minus_eq:
"equal_mod_timpls TI s t ⟷ equal_mod_timpls (filter (λ(a,b). a ≠ b) TI) s t"
(is "?A ⟷ ?B")
proof
show ?A when ?B using that equal_mod_timpls_mono[of "filter (λ(a,b). a ≠ b) TI" TI] by auto
show ?B when ?A using that
proof (induction TI s t rule: equal_mod_timpls.induct)
case (2 TI f T g S)
define TI' where "TI' ≡ filter (λ(a,b). a ≠ b) TI"
let ?P = "λX Y. f = g ∨ (is_Abs f ∧ is_Abs g ∧ ((the_Abs f, the_Abs g) ∈ set X ∨
(the_Abs g, the_Abs f) ∈ set X ∨ (∃ti ∈ set Y.
(the_Abs f, snd ti) ∈ set X ∧ (the_Abs g, snd ti) ∈ set X)))"
have *: "?P TI TI" "list_all2 (equal_mod_timpls TI) T S"
using "2.prems" by simp_all
have "?P TI' TI"
using *(1) unfolding TI'_def is_Abs_def by auto
hence "?P TI' TI'"
by (metis (no_types, lifting) snd_conv)
moreover have "list_all2 (equal_mod_timpls TI') T S"
using *(2) "2.IH" list.rel_mono_strong unfolding TI'_def by blast
ultimately show ?case unfolding TI'_def by force
qed auto
qed
lemma timpls_transformable_to_refl:
"timpls_transformable_to TI t t" (is ?A)
"timpls_transformable_to' TI t t" (is ?B)
by (induct t) (auto simp add: list_all2_conv_all_nth)
lemma timpls_transformable_to_inv_Var:
"timpls_transformable_to TI (Var x) t ⟹ t = Var x" (is "?A ⟹ ?C")
"timpls_transformable_to TI t (Var x) ⟹ t = Var x" (is "?B ⟹ ?C")
"timpls_transformable_to' TI (Var x) t ⟹ t = Var x" (is "?A' ⟹ ?C")
"timpls_transformable_to' TI t (Var x) ⟹ t = Var x" (is "?B' ⟹ ?C")
by (cases t; auto)+
lemma timpls_transformable_to_inv:
assumes "timpls_transformable_to TI (Fun f T) (Fun g S)"
shows "length T = length S"
and "⋀i. i < length T ⟹ timpls_transformable_to TI (T ! i) (S ! i)"
and "f ≠ g ⟹ (is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ set TI)"
using assms list_all2_conv_all_nth[of "timpls_transformable_to TI" T S] by auto
lemma timpls_transformable_to'_inv:
assumes "timpls_transformable_to' TI (Fun f T) (Fun g S)"
shows "length T = length S"
and "⋀i. i < length T ⟹ timpls_transformable_to' TI (T ! i) (S ! i)"
and "f ≠ g ⟹ (is_Abs f ∧ is_Abs g ∧ in_trancl TI (the_Abs f) (the_Abs g))"
using assms list_all2_conv_all_nth[of "timpls_transformable_to' TI" T S] by auto
lemma timpls_transformable_to_inv':
assumes "timpls_transformable_to TI (Fun f T) t"
shows "is_Fun t"
and "length T = length (args t)"
and "⋀i. i < length T ⟹ timpls_transformable_to TI (T ! i) (args t ! i)"
and "f ≠ the_Fun t ⟹ (
is_Abs f ∧ is_Abs (the_Fun t) ∧ (the_Abs f, the_Abs (the_Fun t)) ∈ set TI)"
and "¬is_Abs f ⟹ f = the_Fun t"
using assms list_all2_conv_all_nth[of "timpls_transformable_to TI" T]
by (cases t; auto)+
lemma timpls_transformable_to'_inv':
assumes "timpls_transformable_to' TI (Fun f T) t"
shows "is_Fun t"
and "length T = length (args t)"
and "⋀i. i < length T ⟹ timpls_transformable_to' TI (T ! i) (args t ! i)"
and "f ≠ the_Fun t ⟹ (
is_Abs f ∧ is_Abs (the_Fun t) ∧ in_trancl TI (the_Abs f) (the_Abs (the_Fun t)))"
and "¬is_Abs f ⟹ f = the_Fun t"
using assms list_all2_conv_all_nth[of "timpls_transformable_to' TI" T]
by (cases t; auto)+
lemma timpls_transformable_to_size_eq:
fixes s t::"(('a, 'b, 'c, 'd) prot_fun, 'e) term"
shows "timpls_transformable_to TI s t ⟹ size s = size t" (is "?A ⟹ ?C")
and "timpls_transformable_to' TI s t ⟹ size s = size t" (is "?B ⟹ ?C")
proof -
have *: "size_list size T = size_list size S"
when "length T = length S" "⋀i. i < length T ⟹ size (T ! i) = size (S ! i)"
for S T::"(('a, 'b, 'c, 'd) prot_fun, 'e) term list"
using that
proof (induction T arbitrary: S)
case (Cons x T')
then obtain y S' where y: "S = y#S'" by (cases S) auto
hence "size_list size T' = size_list size S'" "size x = size y"
using Cons.prems Cons.IH[of S'] by force+
thus ?case using y by simp
qed simp
show ?C when ?A using that
proof (induction rule: timpls_transformable_to.induct)
case (2 TI f T g S)
hence "length T = length S" "⋀i. i < length T ⟹ size (T ! i) = size (S ! i)"
using timpls_transformable_to_inv(1,2)[of TI f T g S] by auto
thus ?case using *[of S T] by simp
qed simp_all
show ?C when ?B using that
proof (induction rule: timpls_transformable_to.induct)
case (2 TI f T g S)
hence "length T = length S" "⋀i. i < length T ⟹ size (T ! i) = size (S ! i)"
using timpls_transformable_to'_inv(1,2)[of TI f T g S] by auto
thus ?case using *[of S T] by simp
qed simp_all
qed
lemma timpls_transformable_to_if_term_variants:
fixes s t::"(('a, 'b, 'c, 'd) prot_fun, 'e) term" and a b::"'c set"
defines "P ≡ (λ_. [])(Abs a := [Abs b])"
assumes st: "term_variants_pred P s t"
and ab: "(a,b) ∈ set TI"
shows "timpls_transformable_to TI s t"
using st P_def
proof (induction rule: term_variants_pred.induct)
case (term_variants_P T S f) thus ?case
using ab list_all2_conv_all_nth[of "timpls_transformable_to TI" T S]
by auto
next
case (term_variants_Fun T S f) thus ?case
using ab list_all2_conv_all_nth[of "timpls_transformable_to TI" T S]
by auto
qed simp
lemma timpls_transformable_to'_if_term_variants:
fixes s t::"(('a, 'b, 'c, 'd) prot_fun, 'e) term" and a b::"'c set"
defines "P ≡ (λ_. [])(Abs a := [Abs b])"
assumes st: "term_variants_pred P s t"
and ab: "(a,b) ∈ (set TI)⇧+"
shows "timpls_transformable_to' TI s t"
using st P_def
proof (induction rule: term_variants_pred.induct)
case (term_variants_P T S f) thus ?case
using ab list_all2_conv_all_nth[of "timpls_transformable_to' TI" T S]
in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
by auto
next
case (term_variants_Fun T S f) thus ?case
using ab list_all2_conv_all_nth[of "timpls_transformable_to' TI" T S]
in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
by auto
qed simp
lemma timpls_transformable_to_trans:
assumes TI_trancl: "∀(a,b) ∈ (set TI)⇧+. a ≠ b ⟶ (a,b) ∈ set TI"
and st: "timpls_transformable_to TI s t"
and tu: "timpls_transformable_to TI t u"
shows "timpls_transformable_to TI s u"
using st tu
proof (induction s arbitrary: t u)
case (Var x) thus ?case using tu timpls_transformable_to_inv_Var(1) by fast
next
case (Fun f T)
obtain g S where t:
"t = Fun g S" "length T = length S"
"⋀i. i < length T ⟹ timpls_transformable_to TI (T ! i) (S ! i)"
"f ≠ g ⟹ is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ set TI"
using timpls_transformable_to_inv'[OF Fun.prems(1)] TI_trancl by auto
obtain h U where u:
"u = Fun h U" "length S = length U"
"⋀i. i < length S ⟹ timpls_transformable_to TI (S ! i) (U ! i)"
"g ≠ h ⟹ is_Abs g ∧ is_Abs h ∧ (the_Abs g, the_Abs h) ∈ set TI"
using timpls_transformable_to_inv'[OF Fun.prems(2)[unfolded t(1)]] TI_trancl by auto
have "list_all2 (timpls_transformable_to TI) T U"
using t(1,2,3) u(1,2,3) Fun.IH
list_all2_conv_all_nth[of "timpls_transformable_to TI" T S]
list_all2_conv_all_nth[of "timpls_transformable_to TI" S U]
list_all2_conv_all_nth[of "timpls_transformable_to TI" T U]
by force
moreover have "(the_Abs f, the_Abs h) ∈ set TI"
when "(the_Abs f, the_Abs g) ∈ set TI" "(the_Abs g, the_Abs h) ∈ set TI"
"f ≠ h" "is_Abs f" "is_Abs h"
using that(3,4,5) TI_trancl trancl_into_trancl[OF r_into_trancl[OF that(1)] that(2)]
unfolding is_Abs_def the_Abs_def
by force
hence "is_Abs f ∧ is_Abs h ∧ (the_Abs f, the_Abs h) ∈ set TI"
when "f ≠ h"
using that TI_trancl t(4) u(4) by fast
ultimately show ?case using t(1) u(1) by force
qed
lemma timpls_transformable_to'_trans:
assumes st: "timpls_transformable_to' TI s t"
and tu: "timpls_transformable_to' TI t u"
shows "timpls_transformable_to' TI s u"
using st tu
proof (induction s arbitrary: t u)
case (Var x) thus ?case using tu timpls_transformable_to_inv_Var(3) by fast
next
case (Fun f T)
note 0 = in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
obtain g S where t:
"t = Fun g S" "length T = length S"
"⋀i. i < length T ⟹ timpls_transformable_to' TI (T ! i) (S ! i)"
"f ≠ g ⟹ is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ (set TI)⇧+"
using timpls_transformable_to'_inv'[OF Fun.prems(1)] 0 by auto
obtain h U where u:
"u = Fun h U" "length S = length U"
"⋀i. i < length S ⟹ timpls_transformable_to' TI (S ! i) (U ! i)"
"g ≠ h ⟹ is_Abs g ∧ is_Abs h ∧ (the_Abs g, the_Abs h) ∈ (set TI)⇧+"
using timpls_transformable_to'_inv'[OF Fun.prems(2)[unfolded t(1)]] 0 by auto
have "list_all2 (timpls_transformable_to' TI) T U"
using t(1,2,3) u(1,2,3) Fun.IH
list_all2_conv_all_nth[of "timpls_transformable_to' TI" T S]
list_all2_conv_all_nth[of "timpls_transformable_to' TI" S U]
list_all2_conv_all_nth[of "timpls_transformable_to' TI" T U]
by force
moreover have "(the_Abs f, the_Abs h) ∈ (set TI)⇧+"
when "(the_Abs f, the_Abs g) ∈ (set TI)⇧+" "(the_Abs g, the_Abs h) ∈ (set TI)⇧+"
using that by simp
hence "is_Abs f ∧ is_Abs h ∧ (the_Abs f, the_Abs h) ∈ (set TI)⇧+"
when "f ≠ h"
by (metis that t(4) u(4))
ultimately show ?case using t(1) u(1) 0 by force
qed
lemma timpls_transformable_to_mono:
assumes "set TI ⊆ set TI'"
and "timpls_transformable_to TI s t"
shows "timpls_transformable_to TI' s t"
using assms
proof (induction TI s t rule: timpls_transformable_to.induct)
case (2 TI f T g S)
have *: "f = g ∨ (is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ set TI)"
"list_all2 (timpls_transformable_to TI) T S"
using "2.prems" by simp_all
show ?case
using "2.IH" "2.prems"(1) list.rel_mono_strong[OF *(2)] *(1) in_trancl_mono[of TI TI']
by (metis (no_types, lifting) timpls_transformable_to.simps(2) set_rev_mp)
qed auto
lemma timpls_transformable_to'_mono:
assumes "set TI ⊆ set TI'"
and "timpls_transformable_to' TI s t"
shows "timpls_transformable_to' TI' s t"
using assms
proof (induction TI s t rule: timpls_transformable_to'.induct)
case (2 TI f T g S)
have *: "f = g ∨ (is_Abs f ∧ is_Abs g ∧ in_trancl TI (the_Abs f) (the_Abs g))"
"list_all2 (timpls_transformable_to' TI) T S"
using "2.prems" by simp_all
show ?case
using "2.IH" "2.prems"(1) list.rel_mono_strong[OF *(2)] *(1) in_trancl_mono[of TI TI']
by (metis (no_types, lifting) timpls_transformable_to'.simps(2))
qed auto
lemma timpls_transformable_to_refl_minus_eq:
"timpls_transformable_to TI s t ⟷ timpls_transformable_to (filter (λ(a,b). a ≠ b) TI) s t"
(is "?A ⟷ ?B")
proof
let ?TI' = "λTI. filter (λ(a,b). a ≠ b) TI"
show ?A when ?B using that timpls_transformable_to_mono[of "?TI' TI" TI] by auto
show ?B when ?A using that
proof (induction TI s t rule: timpls_transformable_to.induct)
case (2 TI f T g S)
have *: "f = g ∨ (is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ set TI)"
"list_all2 (timpls_transformable_to TI) T S"
using "2.prems" by simp_all
have "f = g ∨ (is_Abs f ∧ is_Abs g ∧ (the_Abs f, the_Abs g) ∈ set (?TI' TI))"
using *(1) unfolding is_Abs_def by auto
moreover have "list_all2 (timpls_transformable_to (?TI' TI)) T S"
using *(2) "2.IH" list.rel_mono_strong by blast
ultimately show ?case by force
qed auto
qed
lemma timpls_transformable_to_iff_in_timpl_closure:
assumes "set TI' = {(a,b) ∈ (set TI)⇧+. a ≠ b}"
shows "timpls_transformable_to TI' s t ⟷ t ∈ timpl_closure s (set TI)" (is "?A s t ⟷ ?B s t")
proof
show "?A s t ⟹ ?B s t" using assms
proof (induction s t rule: timpls_transformable_to.induct)
case (2 TI f T g S)
note prems = "2.prems"
note IH = "2.IH"
have 1: "length T = length S" "∀i<length T. timpls_transformable_to TI' (T ! i) (S ! i)"
using prems(1) list_all2_conv_all_nth[of "timpls_transformable_to TI'" T S] by simp_all
note 2 = timpl_closure_is_timpl_closure'
note 3 = in_set_conv_nth[of _ T] in_set_conv_nth[of _ S]
have 4: "timpl_closure' (set TI') = timpl_closure' (set TI)"
using timpl_closure'_timpls_trancl_eq'[of "set TI"] prems(2) by simp
have IH': "(T ! i, S ! i) ∈ timpl_closure' (set TI')" when i: "i < length S" for i
proof -
have "timpls_transformable_to TI' (T ! i) (S ! i)" using i 1 by presburger
hence "S ! i ∈ timpl_closure (T ! i) (set TI)"
using IH[of "T ! i" "S ! i"] i 1(1) prems(2) by force
thus ?thesis using 2[of "S ! i" "T ! i" "set TI"] 4 by blast
qed
have 5: "f = g ∨ (∃a b. (a, b) ∈ (set TI')⇧+ ∧ f = Abs a ∧ g = Abs b)"
using prems(1) the_Abs_def[of f] the_Abs_def[of g] is_Abs_def[of f] is_Abs_def[of g]
by fastforce
show ?case using 2 4 timpl_closure_FunI[OF IH' 1(1) 5] 1(1) by auto
qed (simp_all add: timpl_closure.FP)
show "?B s t ⟹ ?A s t"
proof (induction t rule: timpl_closure.induct)
case (TI u a b v) show ?case
proof (cases "a = b")
case True thus ?thesis using TI.hyps(3) TI.IH term_variants_pred_refl_inv by fastforce
next
case False
hence 1: "timpls_transformable_to TI' u v"
using TI.hyps(2) assms timpls_transformable_to_if_term_variants[OF TI.hyps(3), of TI']
by blast
have 2: "(c,d) ∈ set TI'" when cd: "(c,d) ∈ (set TI')⇧+" "c ≠ d" for c d
proof -
let ?cl = "λX. {(a,b) ∈ X⇧+. a ≠ b}"
have "?cl (set TI') = ?cl (?cl (set TI))" using assms by presburger
hence "set TI' = ?cl (set TI')" using assms trancl_minus_refl_idem[of "set TI"] by argo
thus ?thesis using cd by blast
qed
show ?thesis using timpls_transformable_to_trans[OF _ TI.IH 1] 2 by blast
qed
qed (use timpls_transformable_to_refl in fast)
qed
lemma timpls_transformable_to'_iff_in_timpl_closure:
"timpls_transformable_to' TI s t ⟷ t ∈ timpl_closure s (set TI)" (is "?A s t ⟷ ?B s t")
proof
show "?A s t ⟹ ?B s t"
proof (induction s t rule: timpls_transformable_to'.induct)
case (2 TI f T g S)
note prems = "2.prems"
note IH = "2.IH"
have 1: "length T = length S" "∀i<length T. timpls_transformable_to' TI (T ! i) (S ! i)"
using prems list_all2_conv_all_nth[of "timpls_transformable_to' TI" T S] by simp_all
note 2 = timpl_closure_is_timpl_closure'
note 3 = in_set_conv_nth[of _ T] in_set_conv_nth[of _ S]
have IH': "(T ! i, S ! i) ∈ timpl_closure' (set TI)" when i: "i < length S" for i
proof -
have "timpls_transformable_to' TI (T ! i) (S ! i)" using i 1 by presburger
hence "S ! i ∈ timpl_closure (T ! i) (set TI)" using IH[of "T ! i" "S ! i"] i 1(1) by force
thus ?thesis using 2[of "S ! i" "T ! i" "set TI"] by blast
qed
have 4: "f = g ∨ (∃a b. (a, b) ∈ (set TI)⇧+ ∧ f = Abs a ∧ g = Abs b)"
using prems the_Abs_def[of f] the_Abs_def[of g] is_Abs_def[of f] is_Abs_def[of g]
in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
by auto
show ?case using 2 timpl_closure_FunI[OF IH' 1(1) 4] 1(1) by auto
qed (simp_all add: timpl_closure.FP)
show "?B s t ⟹ ?A s t"
proof (induction t rule: timpl_closure.induct)
case (TI u a b v) thus ?case
using timpls_transformable_to'_trans
timpls_transformable_to'_if_term_variants
by blast
qed (use timpls_transformable_to_refl(2) in fast)
qed
lemma equal_mod_timpls_iff_ex_in_timpl_closure:
assumes "set TI' = {(a,b) ∈ TI⇧+. a ≠ b}"
shows "equal_mod_timpls TI' s t ⟷ (∃u. u ∈ timpl_closure s TI ∧ u ∈ timpl_closure t TI)"
(is "?A s t ⟷ ?B s t")
proof
show "?A s t ⟹ ?B s t" using assms
proof (induction s t rule: equal_mod_timpls.induct)
case (2 TI' f T g S)
note prems = "2.prems"
note IH = "2.IH"
have 1: "length T = length S" "∀i<length T. equal_mod_timpls (TI') (T ! i) (S ! i)"
using prems list_all2_conv_all_nth[of "equal_mod_timpls TI'" T S] by simp_all
note 2 = timpl_closure_is_timpl_closure'
note 3 = in_set_conv_nth[of _ T] in_set_conv_nth[of _ S]
have 4: "timpl_closure' (set TI') = timpl_closure' TI"
using timpl_closure'_timpls_trancl_eq'[of TI] prems
by simp
have IH: "∃u. (T ! i, u) ∈ timpl_closure' TI ∧ (S ! i, u) ∈ timpl_closure' TI"
when i: "i < length S" for i
proof -
have "equal_mod_timpls TI' (T ! i) (S ! i)" using i 1 by presburger
hence "∃u. u ∈ timpl_closure (T ! i) TI ∧ u ∈ timpl_closure (S ! i) TI"
using IH[of "T ! i" "S ! i"] i 1(1) prems by force
thus ?thesis using 4 unfolding 2 by blast
qed
let ?P = "λG. f = g ∨ (∃a b. (a, b) ∈ G ∧ f = Abs a ∧ g = Abs b) ∨
(∃a b. (a, b) ∈ G ∧ f = Abs b ∧ g = Abs a) ∨
(∃a b c. (a, c) ∈ G ∧ (b, c) ∈ G ∧ f = Abs a ∧ g = Abs b)"
have "?P (set TI')"
using prems the_Abs_def[of f] the_Abs_def[of g] is_Abs_def[of f] is_Abs_def[of g]
by fastforce
hence "?P (TI⇧+)" unfolding prems by blast
hence "?P (rtrancl TI)" by (metis (no_types, lifting) trancl_into_rtrancl)
hence 5: "f = g ∨ (∃a b c. (a, c) ∈ TI⇧* ∧ (b, c) ∈ TI⇧* ∧ f = Abs a ∧ g = Abs b)" by blast
show ?case
using timpl_closure_FunI3[OF _ 1(1) 5] IH 1(1)
unfolding timpl_closure'_timpls_rtrancl_eq 2
by auto
qed (use timpl_closure.FP in auto)
show "?A s t" when B: "?B s t"
proof -
obtain u where u: "u ∈ timpl_closure s TI" "u ∈ timpl_closure t TI"
using B by blast
thus ?thesis using assms
proof (induction u arbitrary: s t rule: term.induct)
case (Var x s t) thus ?case
using timpl_closure_Var_in_iff[of x s TI]
timpl_closure_Var_in_iff[of x t TI]
equal_mod_timpls.simps(1)[of TI' x x]
by blast
next
case (Fun f U s t)
obtain g S where s:
"s = Fun g S" "length U = length S"
"⋀i. i < length U ⟹ U ! i ∈ timpl_closure (S ! i) TI"
"g ≠ f ⟹ is_Abs g ∧ is_Abs f ∧ (the_Abs g, the_Abs f) ∈ TI⇧+"
using Fun.prems(1) timpl_closure_Fun_inv'[of f U _ _ TI]
by (cases s) auto
obtain h T where t:
"t = Fun h T" "length U = length T"
"⋀i. i < length U ⟹ U ! i ∈ timpl_closure (T ! i) TI"
"h ≠ f ⟹ is_Abs h ∧ is_Abs f ∧ (the_Abs h, the_Abs f) ∈ TI⇧+"
using Fun.prems(2) timpl_closure_Fun_inv'[of f U _ _ TI]
by (cases t) auto
have g: "(the_Abs g, the_Abs f) ∈ set TI'" "is_Abs f" "is_Abs g" when neq_f: "g ≠ f"
proof -
obtain ga fa where a: "g = Abs ga" "f = Abs fa"
using s(4)[OF neq_f] unfolding is_Abs_def by presburger
hence "the_Abs g ≠ the_Abs f" using neq_f by simp
thus "(the_Abs g, the_Abs f) ∈ set TI'" "is_Abs f" "is_Abs g"
using s(4)[OF neq_f] Fun.prems by blast+
qed
have h: "(the_Abs h, the_Abs f) ∈ set TI'" "is_Abs f" "is_Abs h" when neq_f: "h ≠ f"
proof -
obtain ha fa where a: "h = Abs ha" "f = Abs fa"
using t(4)[OF neq_f] unfolding is_Abs_def by presburger
hence "the_Abs h ≠ the_Abs f" using neq_f by simp
thus "(the_Abs h, the_Abs f) ∈ set TI'" "is_Abs f" "is_Abs h"
using t(4)[OF neq_f] Fun.prems by blast+
qed
have "equal_mod_timpls TI' (S ! i) (T ! i)"
when i: "i < length U" for i
using i Fun.IH s(1,2,3) t(1,2,3) nth_mem[OF i] Fun.prems by meson
hence "list_all2 (equal_mod_timpls TI') S T"
using list_all2_conv_all_nth[of "equal_mod_timpls TI'" S T] s(2) t(2) by presburger
thus ?case using s(1) t(1) g h by fastforce
qed
qed
qed
context
begin
private inductive timpls_transformable_to_pred where
Var: "timpls_transformable_to_pred A (Var x) (Var x)"
| Fun: "⟦¬is_Abs f; length T = length S;
⋀i. i < length T ⟹ timpls_transformable_to_pred A (T ! i) (S ! i)⟧
⟹ timpls_transformable_to_pred A (Fun f T) (Fun f S)"
| Abs: "b ∈ A ⟹ timpls_transformable_to_pred A (Fun (Abs a) []) (Fun (Abs b) [])"
private lemma timpls_transformable_to_pred_inv_Var:
assumes "timpls_transformable_to_pred A (Var x) t"
shows "t = Var x"
using assms by (auto elim: timpls_transformable_to_pred.cases)
private lemma timpls_transformable_to_pred_inv:
assumes "timpls_transformable_to_pred A (Fun f T) t"
shows "is_Fun t"
and "length T = length (args t)"
and "⋀i. i < length T ⟹ timpls_transformable_to_pred A (T ! i) (args t ! i)"
and "¬is_Abs f ⟹ f = the_Fun t"
and "is_Abs f ⟹ (is_Abs (the_Fun t) ∧ the_Abs (the_Fun t) ∈ A)"
using assms by (auto elim!: timpls_transformable_to_pred.cases[of A])
private lemma timpls_transformable_to_pred_finite_aux1:
assumes f: "¬is_Abs f"
shows "{s. timpls_transformable_to_pred A (Fun f T) s} ⊆
(λS. Fun f S) ` {S. length T = length S ∧
(∀s ∈ set S. ∃t ∈ set T. timpls_transformable_to_pred A t s)}"
(is "?B ⊆ ?C")
proof
fix s assume s: "s ∈ ?B"
hence *: "timpls_transformable_to_pred A (Fun f T) s" by blast
obtain S where S:
"s = Fun f S" "length T = length S" "⋀i. i < length T ⟹ timpls_transformable_to_pred A (T ! i) (S ! i)"
using f timpls_transformable_to_pred_inv[OF *] unfolding the_Abs_def is_Abs_def by auto
have "∀s∈set S. ∃t∈set T. timpls_transformable_to_pred A t s" using S(2,3) in_set_conv_nth by metis
thus "s ∈ ?C" using S(1,2) by blast
qed
private lemma timpls_transformable_to_pred_finite_aux2:
"{s. timpls_transformable_to_pred A (Fun (Abs a) []) s} ⊆ (λb. Fun (Abs b) []) ` A" (is "?B ⊆ ?C")
proof
fix s assume s: "s ∈ ?B"
hence *: "timpls_transformable_to_pred A (Fun (Abs a) []) s" by blast
obtain b where b: "s = Fun (Abs b) []" "b ∈ A"
using timpls_transformable_to_pred_inv[OF *] unfolding the_Abs_def is_Abs_def by auto
thus "s ∈ ?C" by blast
qed
private lemma timpls_transformable_to_pred_finite:
fixes t::"(('fun,'atom,'sets,'lbl) prot_fun, 'a) term"
assumes A: "finite A"
and t: "wf⇩t⇩r⇩m t"
shows "finite {s. timpls_transformable_to_pred A t s}"
using t
proof (induction t)
case (Var x)
have "{s::(('fun,'atom,'sets,'lbl) prot_fun, 'a) term. timpls_transformable_to_pred A (Var x) s} = {Var x}"
by (auto intro: timpls_transformable_to_pred.Var elim: timpls_transformable_to_pred_inv_Var)
thus ?case by simp
next
case (Fun f T)
have IH: "finite {s. timpls_transformable_to_pred A t s}" when t: "t ∈ set T" for t
using Fun.IH[OF t] wf_trm_param[OF Fun.prems t] by blast
show ?case
proof (cases "is_Abs f")
case True
then obtain a where a: "f = Abs a" unfolding is_Abs_def by presburger
hence "T = []" using wf_trm_arity[OF Fun.prems] by simp_all
hence "{a. timpls_transformable_to_pred A (Fun f T) a} ⊆ (λb. Fun (Abs b) []) ` A"
using timpls_transformable_to_pred_finite_aux2[of A a] a by auto
thus ?thesis using A finite_subset by fast
next
case False thus ?thesis
using IH finite_lists_length_eq' timpls_transformable_to_pred_finite_aux1[of f A T] finite_subset
by blast
qed
qed
private lemma timpls_transformable_to_pred_if_timpls_transformable_to:
assumes s: "timpls_transformable_to TI t s"
and t: "wf⇩t⇩r⇩m t" "∀f ∈ funs_term t. is_Abs f ⟶ the_Abs f ∈ A"
shows "timpls_transformable_to_pred (A ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+) t s"
using s t
proof (induction rule: timpls_transformable_to.induct)
case (2 TI f T g S)
let ?A = "A ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+"
note prems = "2.prems"
note IH = "2.IH"
note 0 = timpls_transformable_to_inv[OF prems(1)]
have 1: "T = []" "S = []" when f: "f = Abs a" for a
using f wf_trm_arity[OF prems(2)] 0(1) by simp_all
have "∀f ∈ funs_term t. is_Abs f ⟶ the_Abs f ∈ A" when t: "t ∈ set T" for t
using t prems(3) funs_term_subterms_eq(1)[of "Fun f T"] by blast
hence 2: "timpls_transformable_to_pred ?A (T ! i) (S ! i)"
when i: "i < length T" for i
using i IH 0(1,2) wf_trm_param[OF prems(2)]
by (metis (no_types) in_set_conv_nth)
have 3: "the_Abs f ∈ ?A" when f: "is_Abs f" using prems(3) f by force
show ?case
proof (cases "f = g")
case True
note fg = True
show ?thesis
proof (cases "is_Abs f")
case True
then obtain a where a: "f = Abs a" unfolding is_Abs_def by blast
thus ?thesis using fg 1[OF a] timpls_transformable_to_pred.Abs[of a ?A a] 3 by simp
qed (use fg timpls_transformable_to_pred.Fun[OF _ 0(1) 2, of f] in blast)
next
case False
then obtain a b where ab: "f = Abs a" "g = Abs b" "(a, b) ∈ (set TI)⇧+"
using 0(3) in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
unfolding is_Abs_def the_Abs_def by fastforce
hence "a ∈ ?A" "b ∈ ?A" by force+
thus ?thesis using timpls_transformable_to_pred.Abs ab(1,2) 1[OF ab(1)] by metis
qed
qed (simp_all add: timpls_transformable_to_pred.Var)
private lemma timpls_transformable_to_pred_if_timpls_transformable_to':
assumes s: "timpls_transformable_to' TI t s"
and t: "wf⇩t⇩r⇩m t" "∀f ∈ funs_term t. is_Abs f ⟶ the_Abs f ∈ A"
shows "timpls_transformable_to_pred (A ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+) t s"
using s t
proof (induction rule: timpls_transformable_to.induct)
case (2 TI f T g S)
let ?A = "A ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+"
note prems = "2.prems"
note IH = "2.IH"
note 0 = timpls_transformable_to'_inv[OF prems(1)]
have 1: "T = []" "S = []" when f: "f = Abs a" for a
using f wf_trm_arity[OF prems(2)] 0(1) by simp_all
have "∀f ∈ funs_term t. is_Abs f ⟶ the_Abs f ∈ A" when t: "t ∈ set T" for t
using t prems(3) funs_term_subterms_eq(1)[of "Fun f T"] by blast
hence 2: "timpls_transformable_to_pred ?A (T ! i) (S ! i)"
when i: "i < length T" for i
using i IH 0(1,2) wf_trm_param[OF prems(2)]
by (metis (no_types) in_set_conv_nth)
have 3: "the_Abs f ∈ ?A" when f: "is_Abs f" using prems(3) f by force
show ?case
proof (cases "f = g")
case True
note fg = True
show ?thesis
proof (cases "is_Abs f")
case True
then obtain a where a: "f = Abs a" unfolding is_Abs_def by blast
thus ?thesis using fg 1[OF a] timpls_transformable_to_pred.Abs[of a ?A a] 3 by simp
qed (use fg timpls_transformable_to_pred.Fun[OF _ 0(1) 2, of f] in blast)
next
case False
then obtain a b where ab: "f = Abs a" "g = Abs b" "(a, b) ∈ (set TI)⇧+"
using 0(3) in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
unfolding is_Abs_def the_Abs_def by fastforce
hence "a ∈ ?A" "b ∈ ?A" by force+
thus ?thesis using timpls_transformable_to_pred.Abs ab(1,2) 1[OF ab(1)] by metis
qed
qed (simp_all add: timpls_transformable_to_pred.Var)
private lemma timpls_transformable_to_pred_if_equal_mod_timpls:
assumes s: "equal_mod_timpls TI t s"
and t: "wf⇩t⇩r⇩m t" "∀f ∈ funs_term t. is_Abs f ⟶ the_Abs f ∈ A"
shows "timpls_transformable_to_pred (A ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+) t s"
using s t
proof (induction rule: equal_mod_timpls.induct)
case (2 TI f T g S)
let ?A = "A ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+"
note prems = "2.prems"
note IH = "2.IH"
note 0 = equal_mod_timpls_inv[OF prems(1)]
have 1: "T = []" "S = []" when f: "f = Abs a" for a
using f wf_trm_arity[OF prems(2)] 0(1) by simp_all
have "∀f ∈ funs_term t. is_Abs f ⟶ the_Abs f ∈ A" when t: "t ∈ set T" for t
using t prems(3) funs_term_subterms_eq(1)[of "Fun f T"] by blast
hence 2: "timpls_transformable_to_pred ?A (T ! i) (S ! i)"
when i: "i < length T" for i
using i IH 0(1,2) wf_trm_param[OF prems(2)]
by (metis (no_types) in_set_conv_nth)
have 3: "the_Abs f ∈ ?A" when f: "is_Abs f" using prems(3) f by force
show ?case
proof (cases "f = g")
case True
note fg = True
show ?thesis
proof (cases "is_Abs f")
case True
then obtain a where a: "f = Abs a" unfolding is_Abs_def by blast
thus ?thesis using fg 1[OF a] timpls_transformable_to_pred.Abs[of a ?A a] 3 by simp
qed (use fg timpls_transformable_to_pred.Fun[OF _ 0(1) 2, of f] in blast)
next
case False
then obtain a b where ab: "f = Abs a" "g = Abs b"
"(a, b) ∈ (set TI)⇧+ ∨ (b, a) ∈ (set TI)⇧+ ∨
(∃ti ∈ set TI. (a, snd ti) ∈ (set TI)⇧+ ∧ (b, snd ti) ∈ (set TI)⇧+)"
using 0(3) in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
unfolding is_Abs_def the_Abs_def by fastforce
hence "a ∈ ?A" "b ∈ ?A" by force+
thus ?thesis using timpls_transformable_to_pred.Abs ab(1,2) 1[OF ab(1)] by metis
qed
qed (simp_all add: timpls_transformable_to_pred.Var)
lemma timpls_transformable_to_finite:
assumes t: "wf⇩t⇩r⇩m t"
shows "finite {s. timpls_transformable_to TI t s}" (is ?P)
and "finite {s. timpls_transformable_to' TI t s}" (is ?Q)
proof -
let ?A = "the_Abs ` {f ∈ funs_term t. is_Abs f} ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+"
have 0: "finite ?A" by auto
have 1: "{s. timpls_transformable_to TI t s} ⊆ {s. timpls_transformable_to_pred ?A t s}"
using timpls_transformable_to_pred_if_timpls_transformable_to[OF _ t] by auto
have 2: "{s. timpls_transformable_to' TI t s} ⊆ {s. timpls_transformable_to_pred ?A t s}"
using timpls_transformable_to_pred_if_timpls_transformable_to'[OF _ t] by auto
show ?P using timpls_transformable_to_pred_finite[OF 0 t] finite_subset[OF 1] by blast
show ?Q using timpls_transformable_to_pred_finite[OF 0 t] finite_subset[OF 2] by blast
qed
lemma equal_mod_timpls_finite:
assumes t: "wf⇩t⇩r⇩m t"
shows "finite {s. equal_mod_timpls TI t s}"
proof -
let ?A = "the_Abs ` {f ∈ funs_term t. is_Abs f} ∪ fst ` (set TI)⇧+ ∪ snd ` (set TI)⇧+"
have 0: "finite ?A" by auto
have 1: "{s. equal_mod_timpls TI t s} ⊆ {s. timpls_transformable_to_pred ?A t s}"
using timpls_transformable_to_pred_if_equal_mod_timpls[OF _ t] by auto
show ?thesis using timpls_transformable_to_pred_finite[OF 0 t] finite_subset[OF 1] by blast
qed
end
lemma intruder_synth_mod_timpls_is_synth_timpl_closure_set:
fixes t::"(('fun,'atom,'sets,'lbl) prot_fun, 'a) term" and TI TI'
assumes "set TI' = {(a,b) ∈ (set TI)⇧+. a ≠ b}"
shows "intruder_synth_mod_timpls M TI' t ⟷ timpl_closure_set (set M) (set TI) ⊢⇩c t"
(is "?C t ⟷ ?D t")
proof -
have *: "(∃m ∈ M. timpls_transformable_to TI' m t) ⟷ t ∈ timpl_closure_set M (set TI)"
when "set TI' = {(a,b) ∈ (set TI)⇧+. a ≠ b}"
for M TI TI' and t::"(('fun,'atom,'sets,'lbl) prot_fun, 'a) term"
using timpls_transformable_to_iff_in_timpl_closure[OF that]
timpl_closure_set_is_timpl_closure_union[of M "set TI"]
timpl_closure_set_timpls_trancl_eq[of M "set TI"]
timpl_closure_set_timpls_trancl_eq'[of M "set TI"]
by auto
show "?C t ⟷ ?D t"
proof
show "?C t ⟹ ?D t" using assms
proof (induction t arbitrary: M TI TI' rule: intruder_synth_mod_timpls.induct)
case (1 M TI' x)
hence "Var x ∈ timpl_closure_set (set M) (set TI)"
using timpl_closure.FP member_def unfolding timpl_closure_set_def by force
thus ?case by simp
next
case (2 M TI f T)
show ?case
proof (cases "∃m ∈ set M. timpls_transformable_to TI' m (Fun f T)")
case True thus ?thesis
using "2.prems" *[of TI' TI "set M" "Fun f T"]
intruder_synth.AxiomC[of "Fun f T" "timpl_closure_set (set M) (set TI)"]
by blast
next
case False
hence "¬(list_ex (λt. timpls_transformable_to TI' t (Fun f T)) M)"
unfolding list_ex_iff by blast
hence "public f" "length T = arity f" "list_all (intruder_synth_mod_timpls M TI') T"
using "2.prems"(1) by force+
thus ?thesis using "2.IH"[OF _ _ "2.prems"(2)] unfolding list_all_iff by force
qed
qed
show "?D t ⟹ ?C t"
proof (induction t rule: intruder_synth_induct)
case (AxiomC t) thus ?case
using timpl_closure_set_Var_in_iff[of _ "set M" "set TI"] *[OF assms, of "set M" t]
by (cases t rule: term.exhaust) (force simp add: member_def list_ex_iff)+
next
case (ComposeC T f) thus ?case
using list_all_iff[of "intruder_synth_mod_timpls M TI'" T]
intruder_synth_mod_timpls.simps(2)[of M TI' f T]
by blast
qed
qed
qed
lemma intruder_synth_mod_timpls'_is_synth_timpl_closure_set:
fixes t::"(('fun,'atom,'sets,'lbl) prot_fun, 'a) term" and TI
shows "intruder_synth_mod_timpls' M TI t ⟷ timpl_closure_set (set M) (set TI) ⊢⇩c t"
(is "?A t ⟷ ?B t")
proof -
have *: "(∃m ∈ M. timpls_transformable_to' TI m t) ⟷ t ∈ timpl_closure_set M (set TI)"
for M TI and t::"(('fun,'atom,'sets,'lbl) prot_fun, 'a) term"
using timpls_transformable_to'_iff_in_timpl_closure[of TI _ t]
timpl_closure_set_is_timpl_closure_union[of M "set TI"]
by blast+
show "?A t ⟷ ?B t"
proof
show "?A t ⟹ ?B t"
proof (induction t arbitrary: M TI rule: intruder_synth_mod_timpls'.induct)
case (1 M TI x)
hence "Var x ∈ timpl_closure_set (set M) (set TI)"
using timpl_closure.FP List.member_def[of M] unfolding timpl_closure_set_def by auto
thus ?case by simp
next
case (2 M TI f T)
show ?case
proof (cases "∃m ∈ set M. timpls_transformable_to' TI m (Fun f T)")
case True thus ?thesis
using "2.prems" *[of "set M" TI "Fun f T"]
intruder_synth.AxiomC[of "Fun f T" "timpl_closure_set (set M) (set TI)"]
by blast
next
case False
hence "public f" "length T = arity f" "list_all (intruder_synth_mod_timpls' M TI) T"
using "2.prems" list_ex_iff[of _ M] by force+
thus ?thesis
using "2.IH"[of _ M TI] list_all_iff[of "intruder_synth_mod_timpls' M TI" T]
by force
qed
qed
show "?B t ⟹ ?A t"
proof (induction t rule: intruder_synth_induct)
case (AxiomC t) thus ?case
using AxiomC timpl_closure_set_Var_in_iff[of _ "set M" "set TI"] *[of "set M" TI t]
list_ex_iff[of _ M] List.member_def[of M]
by (cases t rule: term.exhaust) force+
next
case (ComposeC T f) thus ?case
using list_all_iff[of "intruder_synth_mod_timpls' M TI" T]
intruder_synth_mod_timpls'.simps(2)[of M TI f T]
by blast
qed
qed
qed
lemma intruder_synth_mod_eq_timpls_is_synth_timpl_closure_set:
fixes t::"(('fun,'atom,'sets,'lbl) prot_fun, 'a) term" and TI
defines "cl ≡ λTI. {(a,b) ∈ TI⇧+. a ≠ b}"
shows "set TI' = {(a,b) ∈ (set TI)⇧+. a ≠ b} ⟹
intruder_synth_mod_eq_timpls M TI' t ⟷
(∃s ∈ timpl_closure t (set TI). timpl_closure_set M (set TI) ⊢⇩c s)"
(is "?Q TI TI' ⟹ ?C t ⟷ ?D t")
proof -
have **: "(∃m ∈ M. equal_mod_timpls TI' m t) ⟷
(∃s ∈ timpl_closure t (set TI). s ∈ timpl_closure_set M (set TI))"
when Q: "?Q TI TI'"
for M TI TI' and t::"(('fun,'atom,'sets,'lbl) prot_fun, 'a) term"
using equal_mod_timpls_iff_ex_in_timpl_closure[OF Q]
timpl_closure_set_is_timpl_closure_union[of M "set TI"]
timpl_closure_set_timpls_trancl_eq'[of M "set TI"]
by fastforce
show "?C t ⟷ ?D t" when Q: "?Q TI TI'"
proof
show "?C t ⟹ ?D t" using Q
proof (induction t arbitrary: M TI rule: intruder_synth_mod_eq_timpls.induct)
case (1 M TI' x M TI)
hence "Var x ∈ timpl_closure_set M (set TI)" "Var x ∈ timpl_closure (Var x) (set TI)"
using timpl_closure.FP unfolding timpl_closure_set_def by auto
thus ?case by force
next
case (2 M TI' f T M TI)
show ?case
proof (cases "∃m ∈ M. equal_mod_timpls TI' m (Fun f T)")
case True thus ?thesis
using **[OF "2.prems"(2), of M "Fun f T"]
intruder_synth.AxiomC[of _ "timpl_closure_set M (set TI)"]
by blast
next
case False
hence f: "public f" "length T = arity f" "list_all (intruder_synth_mod_eq_timpls M TI') T"
using "2.prems" by force+
let ?sy = "intruder_synth (timpl_closure_set M (set TI))"
have IH: "∃u ∈ timpl_closure (T ! i) (set TI). ?sy u"
when i: "i < length T" for i
using "2.IH"[of _ M TI] f(3) nth_mem[OF i] "2.prems"(2)
unfolding list_all_iff by blast
define S where "S ≡ map (λu. SOME v. v ∈ timpl_closure u (set TI) ∧ ?sy v) T"
have S1: "length T = length S"
unfolding S_def by simp
have S2: "S ! i ∈ timpl_closure (T ! i) (set TI)"
"timpl_closure_set M (set TI) ⊢⇩c S ! i"
when i: "i < length S" for i
using i IH someI_ex[of "λv. v ∈ timpl_closure (T ! i) (set TI) ∧ ?sy v"]
unfolding S_def by auto
have "Fun f S ∈ timpl_closure (Fun f T) (set TI)"
using timpl_closure_FunI[of T S "set TI" f f] S1 S2(1)
unfolding timpl_closure_is_timpl_closure' by presburger
thus ?thesis
by (metis intruder_synth.ComposeC[of S f] f(1,2) S1 S2(2) in_set_conv_nth[of _ S])
qed
qed
show "?C t" when D: "?D t"
proof -
obtain s where "timpl_closure_set M (set TI) ⊢⇩c s" "s ∈ timpl_closure t (set TI)"
using D by blast
thus ?thesis
proof (induction s arbitrary: t rule: intruder_synth_induct)
case (AxiomC s t)
note 1 = timpl_closure_set_Var_in_iff[of _ M "set TI"] timpl_closure_Var_inv[of s _ "set TI"]
note 2 = **[OF Q, of M]
show ?case
proof (cases t)
case Var thus ?thesis using 1 AxiomC by auto
next
case Fun thus ?thesis using 2 AxiomC by auto
qed
next
case (ComposeC T f t)
obtain g S where gS:
"t = Fun g S" "length S = length T"
"∀i < length T. T ! i ∈ timpl_closure (S ! i) (set TI)"
"g ≠ f ⟹ is_Abs g ∧ is_Abs f ∧ (the_Abs g, the_Abs f) ∈ (set TI)⇧+"
using ComposeC.prems(1) timpl_closure'_inv'[of t "Fun f T" "set TI"]
timpl_closure_is_timpl_closure'[of _ _ "set TI"]
by fastforce
have IH: "intruder_synth_mod_eq_timpls M TI' u" when u: "u ∈ set S" for u
by (metis u gS(2,3) ComposeC.IH in_set_conv_nth)
note 0 = list_all_iff[of "intruder_synth_mod_eq_timpls M TI'" S]
intruder_synth_mod_eq_timpls.simps(2)[of M TI' g S]
have "f = g" using ComposeC.hyps gS(4) unfolding is_Abs_def by fastforce
thus ?case by (metis ComposeC.hyps(1,2) gS(1,2) IH 0)
qed
qed
qed
qed
lemma timpl_closure_finite:
assumes t: "wf⇩t⇩r⇩m t"
shows "finite (timpl_closure t (set TI))"
using timpls_transformable_to'_iff_in_timpl_closure[of TI t]
timpls_transformable_to_finite[OF t, of TI]
by auto
lemma timpl_closure_set_finite:
fixes TI::"('sets set × 'sets set) list"
assumes M_finite: "finite M"
and M_wf: "wf⇩t⇩r⇩m⇩s M"
shows "finite (timpl_closure_set M (set TI))"
using timpl_closure_set_is_timpl_closure_union[of M "set TI"]
timpl_closure_finite[of _ TI] M_finite M_wf finite
by auto
lemma comp_timpl_closure_is_timpl_closure_set:
fixes M and TI::"('sets set × 'sets set) list"
assumes M_finite: "finite M"
and M_wf: "wf⇩t⇩r⇩m⇩s M"
shows "comp_timpl_closure M (set TI) = timpl_closure_set M (set TI)"
using lfp_while''[OF timpls_Un_mono[of M "set TI"]]
timpl_closure_set_finite[OF M_finite M_wf]
timpl_closure_set_lfp[of M "set TI"]
unfolding comp_timpl_closure_def Let_def by presburger
context
begin
private lemma analyzed_closed_mod_timpls_is_analyzed_closed_timpl_closure_set_aux1:
fixes M::"('fun,'atom,'sets,'lbl) prot_terms"
assumes f: "arity⇩f f = length T" "arity⇩f f > 0" "Ana⇩f f = (K, R)"
and i: "i < length R"
and M: "timpl_closure_set M TI ⊢⇩c T ! (R ! i)"
and m: "Fun (Fu f) T ∈ M"
and t: "Fun (Fu f) S ∈ timpl_closure (Fun (Fu f) T) TI"
shows "timpl_closure_set M TI ⊢⇩c S ! (R ! i)"
proof -
have "R ! i < length T" using i Ana⇩f_assm2_alt[OF f(3)] f(1) by simp
thus ?thesis
using timpl_closure_Fun_inv'(1,2)[OF t] intruder_synth_timpl_closure'[OF M]
by presburger
qed
private lemma analyzed_closed_mod_timpls_is_analyzed_closed_timpl_closure_set_aux2:
fixes M::"('fun,'atom,'sets,'lbl) prot_terms"
assumes M: "∀s ∈ set (snd (Ana m)). timpl_closure_set M TI ⊢⇩c s"
and m: "m ∈ M"
and t: "t ∈ timpl_closure m TI"
and s: "s ∈ set (snd (Ana t))"
shows "timpl_closure_set M TI ⊢⇩c s"
proof -
obtain f S K N where fS: "t = Fun (Fu f) S" "arity⇩f f = length S" "0 < arity⇩f f"
and Ana_f: "Ana⇩f f = (K, N)"
and Ana_t: "Ana t = (K ⋅⇩l⇩i⇩s⇩t (!) S, map ((!) S) N)"
using Ana_nonempty_inv[of t] s by fastforce
then obtain T where T: "m = Fun (Fu f) T" "length T = length S"
using t timpl_closure_Fu_inv'[of f S m TI]
by blast
hence Ana_m: "Ana m = (K ⋅⇩l⇩i⇩s⇩t (!) T, map ((!) T) N)"
using fS(2,3) Ana_f by auto
obtain i where i: "i < length N" "s = S ! (N ! i)"
using s[unfolded fS(1)] Ana_t[unfolded fS(1)] T(2)
in_set_conv_nth[of s "map (λi. S ! i) N"]
by auto
hence "timpl_closure_set M TI ⊢⇩c T ! (N ! i)"
using M[unfolded T(1)] Ana_m[unfolded T(1)] T(2)
by simp
thus ?thesis
using analyzed_closed_mod_timpls_is_analyzed_closed_timpl_closure_set_aux1[
OF fS(2)[unfolded T(2)[symmetric]] fS(3) Ana_f
i(1) _ m[unfolded T(1)] t[unfolded fS(1) T(1)]]
i(2)
by argo
qed
lemma analyzed_closed_mod_timpls_is_analyzed_timpl_closure_set:
fixes M::"('fun,'atom,'sets,'lbl) prot_term list"
assumes TI': "set TI' = {(a,b) ∈ (set TI)⇧+. a ≠ b}"
and M_wf: "wf⇩t⇩r⇩m⇩s (set M)"
shows "analyzed_closed_mod_timpls M TI' ⟷ analyzed (timpl_closure_set (set M) (set TI))"
(is "?A ⟷ ?B")
proof
let ?C = "∀t ∈ timpl_closure_set (set M) (set TI).
analyzed_in t (timpl_closure_set (set M) (set TI))"
let ?P = "λT. ∀t ∈ set T. timpl_closure_set (set M) (set TI) ⊢⇩c t"
let ?Q = "λt. ∀s ∈ comp_timpl_closure {t} (set TI'). case Ana s of (K, R) ⇒ ?P K ⟶ ?P R"
let ?W = "λt. ∀t ∈ set (fst (Ana t)). ∀f ∈ funs_term t. ¬is_Abs f"
let ?V = "λt. ∀s ∈ comp_timpl_closure (set (fst (Ana t))) (set TI').
¬timpl_closure_set (set M) (set TI) ⊢⇩c s"
note defs = analyzed_closed_mod_timpls_def analyzed_in_code
note 0 = intruder_synth_mod_timpls_is_synth_timpl_closure_set[OF TI', of M]
note 1 = timpl_closure_set_is_timpl_closure_union[of _ "set TI"]
have 2: "comp_timpl_closure N (set TI') = timpl_closure_set N (set TI)"
when "wf⇩t⇩r⇩m⇩s N" "finite N" for N::"('fun,'atom,'sets,'lbl) prot_terms"
using that timpl_closure_set_timpls_trancl_eq'[of N "set TI"]
comp_timpl_closure_is_timpl_closure_set[of N TI']
unfolding TI'[symmetric] by presburger
hence 3: "comp_timpl_closure {t} (set TI') ⊆ timpl_closure_set (set M) (set TI)"
when t: "t ∈ set M" "wf⇩t⇩r⇩m t" for t
using t timpl_closure_set_mono[of "{t}" "set M"] by simp
have ?A when C: ?C
unfolding analyzed_closed_mod_timpls_def
intruder_synth_mod_timpls_is_synth_timpl_closure_set[OF TI']
list_all_iff Let_def
proof (intro ballI)
fix t assume t: "t ∈ set M"
show "if ?P (fst (Ana t)) then ?P (snd (Ana t))
else if ?W t then True
else if ?V t then True
else ?Q t" (is ?R)
proof (cases "?P (fst (Ana t))")
case True
hence "?P (snd (Ana t))"
using C timpl_closure_setI[OF t, of "set TI"] prod.exhaust_sel
unfolding analyzed_in_def by blast
thus ?thesis using True by simp
next
case False
have "?Q t" using 3[OF t] C M_wf t unfolding analyzed_in_def by auto
thus ?thesis using False by argo
qed
qed
thus ?A when B: ?B using B analyzed_is_all_analyzed_in by metis
have ?C when A: ?A unfolding analyzed_in_def Let_def
proof (intro ballI allI impI; elim conjE)
fix t K T s
assume t: "t ∈ timpl_closure_set (set M) (set TI)"
and s: "s ∈ set T"
and Ana_t: "Ana t = (K, T)"
and K: "∀k ∈ set K. timpl_closure_set (set M) (set TI) ⊢⇩c k"
obtain m where m: "m ∈ set M" "t ∈ timpl_closure m (set TI)"
using timpl_closure_set_is_timpl_closure_union t by blast
show "timpl_closure_set (set M) (set TI) ⊢⇩c s"
proof (cases "∀k ∈ set (fst (Ana m)). timpl_closure_set (set M) (set TI) ⊢⇩c k")
case True
hence *: "∀r ∈ set (snd (Ana m)). timpl_closure_set (set M) (set TI) ⊢⇩c r"
using m(1) A
unfolding analyzed_closed_mod_timpls_def
intruder_synth_mod_timpls_is_synth_timpl_closure_set[OF TI']
list_all_iff Let_def
by simp
show ?thesis
using K s Ana_t A
analyzed_closed_mod_timpls_is_analyzed_closed_timpl_closure_set_aux2[OF * m]
by simp
next
case False
note F = this
have *: "comp_timpl_closure {m} (set TI') = timpl_closure m (set TI)"
using 2[of "{m}"] timpl_closureton_is_timpl_closure M_wf m(1)
by blast
have "wf⇩t⇩r⇩m⇩s (set (fst (Ana m)))"
using Ana_keys_wf'[of m "fst (Ana m)"] M_wf m(1) surj_pair[of "Ana m"] by fastforce
hence **: "comp_timpl_closure (set (fst (Ana m))) (set TI') =
timpl_closure_set (set (fst (Ana m))) (set TI)"
using 2[of "set (fst (Ana m))"] by blast
have ***: "set K ⊆ timpl_closure_set (set (fst (Ana m))) (set TI)"
"length K = length (fst (Ana m))"
using timpl_closure_Ana_keys_subset[OF m(2) _ Ana_t]
timpl_closure_Ana_keys_length_eq[OF m(2) _ Ana_t]
surj_pair[of "Ana m"]
by fastforce+
show ?thesis
proof (cases "?W m")
case True
hence "fst (Ana t) = fst (Ana m)" using m timpl_closure_Ana_keys_no_Abs_eq_case by fast
thus ?thesis using F K Ana_t by simp
next
case False
note F' = this
show ?thesis
proof (cases "?V m")
case True
hence "∀k ∈ set K. ¬timpl_closure_set (set M) (set TI) ⊢⇩c k"
using F K Ana_t m s *** unfolding ** by blast
thus ?thesis using K F' *** by simp
next
case False
hence "?Q m"
using m(1) A F F'
unfolding analyzed_closed_mod_timpls_def
intruder_synth_mod_timpls_is_synth_timpl_closure_set[OF TI']
list_all_iff Let_def
by auto
thus ?thesis
using * m(2) K s Ana_t
unfolding Let_def by auto
qed
qed
qed
qed
thus ?B when A: ?A using A analyzed_is_all_analyzed_in by metis
qed
lemma analyzed_closed_mod_timpls'_is_analyzed_timpl_closure_set:
fixes M::"('fun,'atom,'sets,'lbl) prot_term list"
assumes M_wf: "wf⇩t⇩r⇩m⇩s (set M)"
shows "analyzed_closed_mod_timpls' M TI ⟷ analyzed (timpl_closure_set (set M) (set TI))"
(is "?A ⟷ ?B")
proof
let ?C = "∀t ∈ timpl_closure_set (set M) (set TI). analyzed_in t (timpl_closure_set (set M) (set TI))"
let ?P = "λT. ∀t ∈ set T. timpl_closure_set (set M) (set TI) ⊢⇩c t"
let ?Q = "λt. ∀s ∈ comp_timpl_closure {t} (set TI). case Ana s of (K, R) ⇒ ?P K ⟶ ?P R"
let ?W = "λt. ∀t ∈ set (fst (Ana t)). ∀f ∈ funs_term t. ¬is_Abs f"
note defs = analyzed_closed_mod_timpls'_def analyzed_in_code
note 0 = intruder_synth_mod_timpls'_is_synth_timpl_closure_set[of M TI]
note 1 = timpl_closure_set_is_timpl_closure_union[of _ "set TI"]
have 2: "comp_timpl_closure {t} (set TI) = timpl_closure_set {t} (set TI)"
when t: "t ∈ set M" "wf⇩t⇩r⇩m t" for t
using t timpl_closure_set_timpls_trancl_eq[of "{t}" "set TI"]
comp_timpl_closure_is_timpl_closure_set[of "{t}"]
by blast
hence 3: "comp_timpl_closure {t} (set TI) ⊆ timpl_closure_set (set M) (set TI)"
when t: "t ∈ set M" "wf⇩t⇩r⇩m t" for t
using t timpl_closure_set_mono[of "{t}" "set M"]
by fast
have ?A when C: ?C
unfolding analyzed_closed_mod_timpls'_def
intruder_synth_mod_timpls'_is_synth_timpl_closure_set
list_all_iff Let_def
proof (intro ballI)
fix t assume t: "t ∈ set M"
show "if ?P (fst (Ana t)) then ?P (snd (Ana t)) else if ?W t then True else ?Q t" (is ?R)
proof (cases "?P (fst (Ana t))")
case True
hence "?P (snd (Ana t))"
using C timpl_closure_setI[OF t, of "set TI"] prod.exhaust_sel
unfolding analyzed_in_def by blast
thus ?thesis using True by simp
next
case False
have "?Q t" using 3[OF t] C M_wf t unfolding analyzed_in_def by auto
thus ?thesis using False by argo
qed
qed
thus ?A when B: ?B using B analyzed_is_all_analyzed_in by metis
have ?C when A: ?A unfolding analyzed_in_def Let_def
proof (intro ballI allI impI; elim conjE)
fix t K T s
assume t: "t ∈ timpl_closure_set (set M) (set TI)"
and s: "s ∈ set T"
and Ana_t: "Ana t = (K, T)"
and K: "∀k ∈ set K. timpl_closure_set (set M) (set TI) ⊢⇩c k"
obtain m where m: "m ∈ set M" "t ∈ timpl_closure m (set TI)"
using timpl_closure_set_is_timpl_closure_union t by blast
show "timpl_closure_set (set M) (set TI) ⊢⇩c s"
proof (cases "∀k ∈ set (fst (Ana m)). timpl_closure_set (set M) (set TI) ⊢⇩c k")
case True
hence *: "∀r ∈ set (snd (Ana m)). timpl_closure_set (set M) (set TI) ⊢⇩c r"
using m(1) A
unfolding analyzed_closed_mod_timpls'_def
intruder_synth_mod_timpls'_is_synth_timpl_closure_set
list_all_iff
by simp
show ?thesis
using K s Ana_t A
analyzed_closed_mod_timpls_is_analyzed_closed_timpl_closure_set_aux2[OF * m]
by simp
next
case False
note F = this
have *: "comp_timpl_closure {m} (set TI) = timpl_closure m (set TI)"
using 2[OF m(1)] timpl_closureton_is_timpl_closure M_wf m(1)
by blast
show ?thesis
proof (cases "?W m")
case True
hence "fst (Ana t) = fst (Ana m)" using m timpl_closure_Ana_keys_no_Abs_eq_case by fast
thus ?thesis using F K Ana_t by simp
next
case False
hence "?Q m"
using m(1) A F
unfolding analyzed_closed_mod_timpls'_def
intruder_synth_mod_timpls'_is_synth_timpl_closure_set
list_all_iff Let_def
by auto
thus ?thesis
using * m(2) K s Ana_t
unfolding Let_def by auto
qed
qed
qed
thus ?B when A: ?A using A analyzed_is_all_analyzed_in by metis
qed
end
end
end