2580 lines
112 KiB
Plaintext
2580 lines
112 KiB
Plaintext
(*
|
|
(C) Copyright Andreas Viktor Hess, DTU, 2020
|
|
(C) Copyright Sebastian A. Mödersheim, DTU, 2020
|
|
(C) Copyright Achim D. Brucker, University of Exeter, 2020
|
|
(C) Copyright Anders Schlichtkrull, DTU, 2020
|
|
|
|
All Rights Reserved.
|
|
|
|
Redistribution and use in source and binary forms, with or without
|
|
modification, are permitted provided that the following conditions are
|
|
met:
|
|
|
|
- Redistributions of source code must retain the above copyright
|
|
notice, this list of conditions and the following disclaimer.
|
|
|
|
- Redistributions in binary form must reproduce the above copyright
|
|
notice, this list of conditions and the following disclaimer in the
|
|
documentation and/or other materials provided with the distribution.
|
|
|
|
- Neither the name of the copyright holder nor the names of its
|
|
contributors may be used to endorse or promote products
|
|
derived from this software without specific prior written
|
|
permission.
|
|
|
|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
|
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
|
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
|
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
|
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
|
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
|
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
|
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
|
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
|
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
|
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|
*)
|
|
|
|
(* Title: Term_Implication.thy
|
|
Author: Andreas Viktor Hess, DTU
|
|
Author: Sebastian A. Mödersheim, DTU
|
|
Author: Achim D. Brucker, University of Exeter
|
|
Author: Anders Schlichtkrull, DTU
|
|
*)
|
|
|
|
section\<open>Term Implication\<close>
|
|
theory Term_Implication
|
|
imports Stateful_Protocol_Model Term_Variants
|
|
begin
|
|
|
|
subsection \<open>Single Term Implications\<close>
|
|
definition timpl_apply_term ("\<langle>_ --\<guillemotright> _\<rangle>\<langle>_\<rangle>") where
|
|
"\<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle> \<equiv> term_variants ((\<lambda>_. [])(Abs a := [Abs b])) t"
|
|
|
|
definition timpl_apply_terms ("\<langle>_ --\<guillemotright> _\<rangle>\<langle>_\<rangle>\<^sub>s\<^sub>e\<^sub>t") where
|
|
"\<langle>a --\<guillemotright> b\<rangle>\<langle>M\<rangle>\<^sub>s\<^sub>e\<^sub>t \<equiv> \<Union>((set o timpl_apply_term a b) ` M)"
|
|
|
|
lemma timpl_apply_Fun:
|
|
assumes "\<And>i. i < length T \<Longrightarrow> S ! i \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>T ! i\<rangle>"
|
|
and "length T = length S"
|
|
shows "Fun f S \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>Fun f T\<rangle>"
|
|
using assms term_variants_Fun term_variants_pred_iff_in_term_variants
|
|
by (metis timpl_apply_term_def)
|
|
|
|
lemma timpl_apply_Abs:
|
|
assumes "\<And>i. i < length T \<Longrightarrow> S ! i \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>T ! i\<rangle>"
|
|
and "length T = length S"
|
|
shows "Fun (Abs b) S \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>Fun (Abs a) T\<rangle>"
|
|
using assms(1) term_variants_P[OF assms(2), of "(\<lambda>_. [])(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 \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle>"
|
|
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) [] \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>Fun (Abs a) []\<rangle>"
|
|
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 \<Longrightarrow> set \<langle>a --\<guillemotright> b\<rangle>\<langle>Fun (Abs c) []\<rangle> = {Fun (Abs b) [], Fun (Abs c) []}"
|
|
"c \<noteq> a \<Longrightarrow> set \<langle>a --\<guillemotright> b\<rangle>\<langle>Fun (Abs c) []\<rangle> = {Fun (Abs c) []}"
|
|
using term_variants_pred_const_cases[of "(\<lambda>_. [])(Abs a := [Abs b])" "Abs c"]
|
|
term_variants_pred_iff_in_term_variants[of "(\<lambda>_. [])(Abs a := [Abs b])"]
|
|
unfolding timpl_apply_term_def by auto
|
|
|
|
lemma timpl_apply_term_subst:
|
|
"s \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle> \<Longrightarrow> s \<cdot> \<delta> \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t \<cdot> \<delta>\<rangle>"
|
|
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 \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>Fun f T\<rangle>"
|
|
shows "length T = length S"
|
|
and "\<And>i. i < length T \<Longrightarrow> S ! i \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>T ! i\<rangle>"
|
|
and "f \<noteq> h \<Longrightarrow> f = Abs a \<and> h = Abs b"
|
|
using assms term_variants_pred_iff_in_term_variants[of "(\<lambda>_. [])(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 \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>Fun f T\<rangle>"
|
|
shows "\<exists>g S. s = Fun g S"
|
|
proof -
|
|
have *: "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (Fun f T) s"
|
|
using assms term_variants_pred_iff_in_term_variants[of "(\<lambda>_. [])(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 \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle> \<longleftrightarrow> t = Var x"
|
|
using term_variants_pred_inv_Var term_variants_pred_iff_in_term_variants
|
|
unfolding timpl_apply_term_def by metis
|
|
|
|
|
|
|
|
subsection \<open>Term Implication Closure\<close>
|
|
inductive_set timpl_closure for t TI where
|
|
FP: "t \<in> timpl_closure t TI"
|
|
| TI: "\<lbrakk>u \<in> timpl_closure t TI; (a,b) \<in> TI; term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) u s\<rbrakk>
|
|
\<Longrightarrow> s \<in> timpl_closure t TI"
|
|
|
|
definition "timpl_closure_set M TI \<equiv> (\<Union>t \<in> M. timpl_closure t TI)"
|
|
|
|
inductive_set timpl_closure'_step for TI where
|
|
"\<lbrakk>(a,b) \<in> TI; term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t s\<rbrakk>
|
|
\<Longrightarrow> (t,s) \<in> timpl_closure'_step TI"
|
|
|
|
definition "timpl_closure' TI \<equiv> (timpl_closure'_step TI)\<^sup>*"
|
|
|
|
definition comp_timpl_closure where
|
|
"comp_timpl_closure FP TI \<equiv>
|
|
let f = \<lambda>X. FP \<union> (\<Union>x \<in> X. \<Union>(a,b) \<in> TI. set \<langle>a --\<guillemotright> b\<rangle>\<langle>x\<rangle>)
|
|
in while (\<lambda>X. f X \<noteq> X) f {}"
|
|
|
|
definition comp_timpl_closure_list where
|
|
"comp_timpl_closure_list FP TI \<equiv>
|
|
let f = \<lambda>X. remdups (concat (map (\<lambda>x. concat (map (\<lambda>(a,b). \<langle>a --\<guillemotright> b\<rangle>\<langle>x\<rangle>) TI)) X))
|
|
in while (\<lambda>X. set (f X) \<noteq> set X) f FP"
|
|
|
|
lemma timpl_closure_setI:
|
|
"t \<in> M \<Longrightarrow> t \<in> 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 \<in> ?A \<Longrightarrow> s \<in> ?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 \<equiv> (\<lambda>_. [])(Abs a := [Abs b])"
|
|
assumes "term_variants_pred P t s" "\<forall>f \<in> funs_term s. \<not>is_Abs f"
|
|
shows "t = s"
|
|
using assms(2,3) P_def
|
|
proof (induction P t s rule: term_variants_pred.induct)
|
|
case (term_variants_Fun T S f)
|
|
have "\<not>is_Abs h" when i: "i < length S" and h: "h \<in> funs_term (S ! i)" for i h
|
|
using i h term_variants_Fun.hyps(4) by auto
|
|
hence "T ! i = S ! i" when i: "i < length T" for i using i term_variants_Fun.hyps(1,3) 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)
|
|
|
|
lemma timpl_closure'_step_inv:
|
|
assumes "(t,s) \<in> timpl_closure'_step TI"
|
|
obtains a b where "(a,b) \<in> TI" "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t s"
|
|
using assms by (auto elim: timpl_closure'_step.cases)
|
|
|
|
lemma timpl_closure_mono:
|
|
assumes "TI \<subseteq> TI'"
|
|
shows "timpl_closure t TI \<subseteq> timpl_closure t TI'"
|
|
proof
|
|
fix s show "s \<in> timpl_closure t TI \<Longrightarrow> s \<in> 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 \<subseteq> M'" "TI \<subseteq> TI'"
|
|
shows "timpl_closure_set M TI \<subseteq> 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 \<in> timpl_closure t TI"
|
|
when "s \<in> timpl_closure u TI" "u \<in> timpl_closure t TI"
|
|
for s u
|
|
using that
|
|
by (induction rule: timpl_closure.induct)
|
|
(auto intro: timpl_closure.intros)
|
|
thus "?A \<subseteq> ?B" unfolding timpl_closure_set_def by blast
|
|
|
|
show "?B \<subseteq> ?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 \<subseteq> timpl_closure_set M TI"
|
|
shows "timpl_closure_set N TI \<subseteq> 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 \<in> timpl_closure t TI \<longleftrightarrow> (t,s) \<in> timpl_closure' TI"
|
|
proof
|
|
show "s \<in> timpl_closure t TI \<Longrightarrow> (t,s) \<in> 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) \<in> timpl_closure' TI \<Longrightarrow> s \<in> 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 \<subseteq> TI'"
|
|
shows "timpl_closure' TI \<subseteq> 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\<^sup>+) \<subseteq> timpl_closure' c"
|
|
unfolding timpl_closure'_def
|
|
proof
|
|
fix s t::"(('a,'b,'c) prot_fun,'d) term"
|
|
show "(s,t) \<in> (timpl_closure'_step (c\<^sup>+))\<^sup>* \<Longrightarrow> (s,t) \<in> (timpl_closure'_step c)\<^sup>*"
|
|
proof (induction rule: rtrancl_induct)
|
|
case (step u t)
|
|
obtain a b where ab:
|
|
"(a,b) \<in> c\<^sup>+" "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) u t"
|
|
using step.hyps(2) timpl_closure'_step_inv by blast
|
|
hence "(u,t) \<in> (timpl_closure'_step c)\<^sup>*"
|
|
proof (induction arbitrary: t rule: trancl_induct)
|
|
case (step d e)
|
|
obtain s where s:
|
|
"term_variants_pred ((\<lambda>_. [])(Abs a := [Abs d])) u s"
|
|
"term_variants_pred ((\<lambda>_. [])(Abs d := [Abs e])) s t"
|
|
using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast
|
|
|
|
have "(u,s) \<in> (timpl_closure'_step c)\<^sup>*"
|
|
"(s,t) \<in> 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) \<in> c\<^sup>+. a \<noteq> b} \<subseteq> timpl_closure' c"
|
|
using timpl_closure'_timpls_trancl_subset
|
|
timpl_closure'_mono[of "{(a,b) \<in> c\<^sup>+. a \<noteq> b}" "c\<^sup>+"]
|
|
by fast
|
|
|
|
lemma timpl_closure_set_timpls_trancl_subset:
|
|
"timpl_closure_set M (c\<^sup>+) \<subseteq> 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\<^sup>+"]
|
|
timpl_closure_set_is_timpl_closure_union[of M c]
|
|
timpl_closure_set_is_timpl_closure_union[of M "c\<^sup>+"]
|
|
by fastforce
|
|
|
|
lemma timpl_closure_set_timpls_trancl_subset':
|
|
"timpl_closure_set M {(a,b) \<in> c\<^sup>+. a \<noteq> b} \<subseteq> 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) \<in> c\<^sup>+. a \<noteq> b}"]
|
|
timpl_closure_set_is_timpl_closure_union[of M c]
|
|
timpl_closure_set_is_timpl_closure_union[of M "{(a,b) \<in> c\<^sup>+. a \<noteq> b}"]
|
|
by fastforce
|
|
|
|
lemma timpl_closure'_timpls_trancl_supset':
|
|
"timpl_closure' c \<subseteq> timpl_closure' {(a,b) \<in> c\<^sup>+. a \<noteq> b}"
|
|
unfolding timpl_closure'_def
|
|
proof
|
|
let ?cl = "{(a,b) \<in> c\<^sup>+. a \<noteq> b}"
|
|
|
|
fix s t::"(('e,'f,'c) prot_fun,'g) term"
|
|
show "(s,t) \<in> (timpl_closure'_step c)\<^sup>* \<Longrightarrow> (s,t) \<in> (timpl_closure'_step ?cl)\<^sup>*"
|
|
proof (induction rule: rtrancl_induct)
|
|
case (step u t)
|
|
obtain a b where ab:
|
|
"(a,b) \<in> c" "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) u t"
|
|
using step.hyps(2) timpl_closure'_step_inv by blast
|
|
hence "(a,b) \<in> c\<^sup>+" by simp
|
|
hence "(u,t) \<in> (timpl_closure'_step ?cl)\<^sup>*" 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 ((\<lambda>_. [])(Abs a := [Abs d])) u s"
|
|
"term_variants_pred ((\<lambda>_. [])(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) \<in> (timpl_closure'_step ?cl)\<^sup>*"
|
|
"(s,t) \<in> 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 \<subseteq> timpl_closure' (c\<^sup>+)"
|
|
using timpl_closure'_timpls_trancl_supset'[of c]
|
|
timpl_closure'_mono[of "{(a,b) \<in> c\<^sup>+. a \<noteq> b}" "c\<^sup>+"]
|
|
by fast
|
|
|
|
lemma timpl_closure'_timpls_trancl_eq:
|
|
"timpl_closure' (c\<^sup>+) = 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) \<in> c\<^sup>+. a \<noteq> 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\<^sup>*) \<subseteq> timpl_closure' c"
|
|
unfolding timpl_closure'_def
|
|
proof
|
|
fix s t::"(('a,'b,'c) prot_fun,'d) term"
|
|
show "(s,t) \<in> (timpl_closure'_step (c\<^sup>*))\<^sup>* \<Longrightarrow> (s,t) \<in> (timpl_closure'_step c)\<^sup>*"
|
|
proof (induction rule: rtrancl_induct)
|
|
case (step u t)
|
|
obtain a b where ab:
|
|
"(a,b) \<in> c\<^sup>*" "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) u t"
|
|
using step.hyps(2) timpl_closure'_step_inv by blast
|
|
hence "(u,t) \<in> (timpl_closure'_step c)\<^sup>*"
|
|
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 ((\<lambda>_. [])(Abs a := [Abs d])) u s"
|
|
"term_variants_pred ((\<lambda>_. [])(Abs d := [Abs e])) s t"
|
|
using term_variants_pred_dense'[OF step.prems, of "Abs d"] by blast
|
|
|
|
have "(u,s) \<in> (timpl_closure'_step c)\<^sup>*"
|
|
"(s,t) \<in> 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 \<subseteq> timpl_closure' (c\<^sup>*)"
|
|
unfolding timpl_closure'_def
|
|
proof
|
|
fix s t::"(('e,'f,'c) prot_fun,'g) term"
|
|
show "(s,t) \<in> (timpl_closure'_step c)\<^sup>* \<Longrightarrow> (s,t) \<in> (timpl_closure'_step (c\<^sup>*))\<^sup>*"
|
|
proof (induction rule: rtrancl_induct)
|
|
case (step u t)
|
|
obtain a b where ab:
|
|
"(a,b) \<in> c" "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) u t"
|
|
using step.hyps(2) timpl_closure'_step_inv by blast
|
|
hence "(a,b) \<in> c\<^sup>*" by simp
|
|
hence "(u,t) \<in> (timpl_closure'_step (c\<^sup>*))\<^sup>*" 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 ((\<lambda>_. [])(Abs a := [Abs d])) u s"
|
|
"term_variants_pred ((\<lambda>_. [])(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) \<in> (timpl_closure'_step (c\<^sup>*))\<^sup>*"
|
|
"(s,t) \<in> timpl_closure'_step (c\<^sup>*)"
|
|
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\<^sup>*) = 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\<^sup>+) = 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\<^sup>+"]
|
|
by fastforce
|
|
|
|
lemma timpl_closure_set_timpls_trancl_eq:
|
|
"timpl_closure_set M (c\<^sup>+) = 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\<^sup>+"]
|
|
by fastforce
|
|
|
|
lemma timpl_closure_set_timpls_trancl_eq':
|
|
"timpl_closure_set M {(a,b) \<in> c\<^sup>+. a \<noteq> 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) \<in> c\<^sup>+. a \<noteq> b}"]
|
|
timpl_closure_set_is_timpl_closure_union[of M c]
|
|
timpl_closure_set_is_timpl_closure_union[of M "{(a,b) \<in> c\<^sup>+. a \<noteq> b}"]
|
|
by fastforce
|
|
|
|
lemma timpl_closure_Var_in_iff:
|
|
"Var x \<in> timpl_closure t TI \<longleftrightarrow> t = Var x" (is "?A \<longleftrightarrow> ?B")
|
|
proof
|
|
have "s \<in> timpl_closure t TI \<Longrightarrow> s = Var x \<Longrightarrow> s = t" for s
|
|
apply (induction rule: timpl_closure.induct)
|
|
by (simp, metis term_variants_pred_inv_Var(2))
|
|
thus "?A \<Longrightarrow> ?B" by blast
|
|
qed (blast intro: timpl_closure.FP)
|
|
|
|
lemma timpl_closure_set_Var_in_iff:
|
|
"Var x \<in> timpl_closure_set M TI \<longleftrightarrow> Var x \<in> M"
|
|
unfolding timpl_closure_set_def by (simp add: timpl_closure_Var_in_iff[of x _ TI])
|
|
|
|
lemma timpl_closure_Var_inv:
|
|
assumes "t \<in> 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 (\<lambda>X. FP \<union> (\<Union>x \<in> X. \<Union>(a,b) \<in> TI. set \<langle>a --\<guillemotright> b\<rangle>\<langle>x\<rangle>))"
|
|
by (auto intro!: monoI)
|
|
|
|
lemma timpl_closure_set_lfp:
|
|
fixes M TI
|
|
defines "f \<equiv> \<lambda>X. M \<union> (\<Union>x \<in> X. \<Union>(a,b) \<in> TI. set \<langle>a --\<guillemotright> b\<rangle>\<langle>x\<rangle>)"
|
|
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 \<subseteq> ?N"
|
|
proof (induction rule: lfp_induct)
|
|
case 2 thus ?case
|
|
proof
|
|
fix t assume "t \<in> f (lfp f \<inter> ?N)"
|
|
hence "t \<in> M \<or> t \<in> (\<Union>x \<in> ?N. \<Union>(a,b) \<in> TI. set \<langle>a --\<guillemotright> b\<rangle>\<langle>x\<rangle>)" (is "?A \<or> ?B")
|
|
unfolding f_def by blast
|
|
thus "t \<in> ?N"
|
|
proof
|
|
assume ?B
|
|
then obtain s a b where s: "s \<in> ?N" "(a,b) \<in> TI" "t \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>s\<rangle>" by moura
|
|
thus ?thesis
|
|
using term_variants_pred_iff_in_term_variants[of "(\<lambda>_. [])(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 \<in> lfp f" when t: "t \<in> timpl_closure s TI" and s: "s \<in> 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 "(\<lambda>_. [])(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 \<subseteq> lfp f" unfolding timpl_closure_set_def by blast
|
|
qed
|
|
|
|
lemma timpl_closure_set_supset:
|
|
assumes "\<forall>t \<in> FP. t \<in> closure"
|
|
and "\<forall>t \<in> closure. \<forall>(a,b) \<in> TI. \<forall>s \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle>. s \<in> closure"
|
|
shows "timpl_closure_set FP TI \<subseteq> closure"
|
|
proof -
|
|
have "t \<in> closure" when t: "t \<in> timpl_closure s TI" and s: "s \<in> 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 "(\<lambda>_. [])(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 "\<forall>t \<in> FP. \<forall>(a,b) \<in> TI. \<forall>s \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle>. s \<in> FP"
|
|
shows "timpl_closure_set FP TI \<subseteq> FP"
|
|
using timpl_closure_set_supset[OF _ assms] by blast
|
|
|
|
lemma timpl_closure'_param:
|
|
assumes "(t,s) \<in> timpl_closure' c"
|
|
and fg: "f = g \<or> (\<exists>a b. (a,b) \<in> c \<and> f = Abs a \<and> g = Abs b)"
|
|
shows "(Fun f (S@t#T), Fun g (S@s#T)) \<in> 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) \<in> c" "f = Abs a" "g = Abs b"
|
|
using fg by moura
|
|
show ?thesis
|
|
using term_variants_pred_param[OF term_variants_pred_refl[of "(\<lambda>_. [])(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) \<in> c" "term_variants_pred ((\<lambda>_. [])(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)) \<in> 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) \<in> timpl_closure' c"
|
|
shows "(Fun f (S@t#T), Fun f (S@s#T)) \<in> timpl_closure' c"
|
|
using timpl_closure'_param[OF assms] by simp
|
|
|
|
lemma timpl_closure_FunI:
|
|
assumes IH: "\<And>i. i < length T \<Longrightarrow> (T ! i, S ! i) \<in> timpl_closure' c"
|
|
and len: "length T = length S"
|
|
and fg: "f = g \<or> (\<exists>a b. (a,b) \<in> c\<^sup>+ \<and> f = Abs a \<and> g = Abs b)"
|
|
shows "(Fun f T, Fun g S) \<in> timpl_closure' c"
|
|
proof -
|
|
have aux: "(Fun f T, Fun g (take n S@drop n T)) \<in> timpl_closure' c"
|
|
when "n \<le> length T" for n
|
|
using that
|
|
proof (induction n)
|
|
case 0
|
|
have "(T ! n, T ! n) \<in> 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) \<in> timpl_closure' c"
|
|
proof (cases "f = g")
|
|
case False
|
|
then obtain a b where ab: "(a, b) \<in> c\<^sup>+" "f = Abs a" "g = Abs b"
|
|
using fg by moura
|
|
show ?thesis
|
|
using timpl_closure'_step.intros[OF ab(1), of "Fun f T" "Fun g T"] ab(2,3)
|
|
term_variants_P[OF _ term_variants_pred_refl[of "(\<lambda>_. [])(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)) \<in> 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) \<in> 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: "\<And>i. i < length T \<Longrightarrow> (T ! i, S ! i) \<in> timpl_closure' c"
|
|
and len: "length T = length S"
|
|
shows "(Fun f T, Fun f S) \<in> timpl_closure' c"
|
|
using timpl_closure_FunI[OF IH len] by simp
|
|
|
|
lemma timpl_closure_FunI2:
|
|
fixes f g::"('a, 'b, 'c) prot_fun"
|
|
assumes IH: "\<And>i. i < length T \<Longrightarrow> \<exists>u. (T!i, u) \<in> timpl_closure' c \<and> (S!i, u) \<in> timpl_closure' c"
|
|
and len: "length T = length S"
|
|
and fg: "f = g \<or> (\<exists>a b d. (a, d) \<in> c\<^sup>+ \<and> (b, d) \<in> c\<^sup>+ \<and> f = Abs a \<and> g = Abs b)"
|
|
shows "\<exists>h U. (Fun f T, Fun h U) \<in> timpl_closure' c \<and> (Fun g S, Fun h U) \<in> timpl_closure' c"
|
|
proof -
|
|
let ?P = "\<lambda>i u. (T ! i, u) \<in> timpl_closure' c \<and> (S ! i, u) \<in> timpl_closure' c"
|
|
|
|
define U where "U \<equiv> map (\<lambda>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) \<in> timpl_closure' c \<and> (S ! i, U ! i) \<in> 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) \<in> c\<^sup>+" "(b, d) \<in> c\<^sup>+" "f = Abs a" "g = Abs b"
|
|
using fg by moura
|
|
|
|
define h::"('a, 'b, 'c) prot_fun" where "h = Abs d"
|
|
|
|
have "f = h \<or> (\<exists>a b. (a, b) \<in> c\<^sup>+ \<and> f = Abs a \<and> h = Abs b)"
|
|
"g = h \<or> (\<exists>a b. (a, b) \<in> c\<^sup>+ \<and> g = Abs a \<and> 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) prot_fun"
|
|
assumes IH: "\<And>i. i < length T \<Longrightarrow> \<exists>u. (T!i, u) \<in> timpl_closure' c \<and> (S!i, u) \<in> timpl_closure' c"
|
|
and len: "length T = length S"
|
|
and fg: "f = g \<or> (\<exists>a b d. (a, d) \<in> c \<and> (b, d) \<in> c \<and> f = Abs a \<and> g = Abs b)"
|
|
shows "\<exists>h U. (Fun f T, Fun h U) \<in> timpl_closure' c \<and> (Fun g S, Fun h U) \<in> 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 \<in> 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\<^sub>t\<^sub>r\<^sub>m t" "\<forall>x \<in> fv t. \<exists>a. \<Gamma>\<^sub>v x = TAtom (Atom a)"
|
|
and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
|
|
shows "timpl_closure (t \<cdot> \<delta>) T = timpl_closure t T \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>"
|
|
proof
|
|
have "s \<in> timpl_closure t T \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>"
|
|
when "s \<in> timpl_closure (t \<cdot> \<delta>) 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' \<in> timpl_closure t T" "u = u' \<cdot> \<delta>" by moura
|
|
|
|
have u'_fv: "\<forall>x \<in> fv u'. \<exists>a. \<Gamma>\<^sub>v x = TAtom (Atom a)"
|
|
using timpl_closure_fv_eq[OF u'(1)] t(2) by simp
|
|
hence u_fv: "\<forall>x \<in> fv u. \<exists>a. \<Gamma>\<^sub>v x = TAtom (Atom a)"
|
|
using u'(2) wt_subst_trm''[OF \<delta>(1)] wt_subst_const_fv_type_eq[OF _ \<delta>(1,2), of u']
|
|
by fastforce
|
|
|
|
have "\<forall>x \<in> fv u' \<union> fv s. (\<exists>y. \<delta> x = Var y) \<or> (\<exists>f. \<delta> x = Fun f [] \<and> Abs a \<noteq> f)"
|
|
proof (intro ballI)
|
|
fix x assume x: "x \<in> fv u' \<union> fv s"
|
|
then obtain c where c: "\<Gamma>\<^sub>v x = TAtom (Atom c)"
|
|
using u'_fv u_fv term_variants_pred_fv_eq[OF TI.hyps(3)]
|
|
by blast
|
|
|
|
show "(\<exists>y. \<delta> x = Var y) \<or> (\<exists>f. \<delta> x = Fun f [] \<and> Abs a \<noteq> f)"
|
|
proof (cases "\<delta> x")
|
|
case (Fun f T)
|
|
hence **: "\<Gamma> (Fun f T) = TAtom (Atom c)" and "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
|
|
using c wt_subst_trm''[OF \<delta>(1), of "Var x"] \<delta>(2)
|
|
by fastforce+
|
|
hence "\<delta> x = Fun f []" using Fun const_type_inv_wf by metis
|
|
thus ?thesis using ** by force
|
|
qed metis
|
|
qed
|
|
hence *: "\<forall>x \<in> fv u' \<union> fv s.
|
|
(\<exists>y. \<delta> x = Var y) \<or> (\<exists>f. \<delta> x = Fun f [] \<and> ((\<lambda>_. [])(Abs a := [Abs b])) f = [])"
|
|
by fastforce
|
|
|
|
obtain s' where s': "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) u' s'" "s = s' \<cdot> \<delta>"
|
|
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 \<cdot> \<delta>) T \<subseteq> timpl_closure t T \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>" by fast
|
|
|
|
have "s \<in> timpl_closure (t \<cdot> \<delta>) T"
|
|
when s: "s \<in> timpl_closure t T \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>" for s
|
|
proof -
|
|
obtain s' where s': "s' \<in> timpl_closure t T" "s = s' \<cdot> \<delta>" using s by moura
|
|
have "s' \<cdot> \<delta> \<in> timpl_closure (t \<cdot> \<delta>) T" using s'(1)
|
|
proof (induction s' rule: timpl_closure.induct)
|
|
case FP thus ?case using timpl_closure.FP[of "t \<cdot> \<delta>" 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 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<subseteq> timpl_closure (t \<cdot> \<delta>) T" by fast
|
|
qed
|
|
|
|
lemma (in stateful_protocol_model) timpl_closure_subst_subset:
|
|
assumes t: "t \<in> M"
|
|
and M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M" "\<forall>x \<in> fv\<^sub>s\<^sub>e\<^sub>t M. \<exists>a. \<Gamma>\<^sub>v x = TAtom (Atom a)"
|
|
and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" "ground (subst_range \<delta>)" "subst_domain \<delta> \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
and M_supset: "timpl_closure t T \<subseteq> M"
|
|
shows "timpl_closure (t \<cdot> \<delta>) T \<subseteq> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>"
|
|
proof -
|
|
have t': "wf\<^sub>t\<^sub>r\<^sub>m t" "\<forall>x \<in> fv t. \<exists>a. \<Gamma>\<^sub>v x = TAtom (Atom a)" using t M by auto
|
|
show ?thesis using timpl_closure_subst[OF t' \<delta>(1,2), of T] M_supset by blast
|
|
qed
|
|
|
|
lemma (in stateful_protocol_model) timpl_closure_set_subst_subset:
|
|
assumes M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M" "\<forall>x \<in> fv\<^sub>s\<^sub>e\<^sub>t M. \<exists>a. \<Gamma>\<^sub>v x = TAtom (Atom a)"
|
|
and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" "ground (subst_range \<delta>)" "subst_domain \<delta> \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
and M_supset: "timpl_closure_set M T \<subseteq> M"
|
|
shows "timpl_closure_set (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>) T \<subseteq> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>"
|
|
using timpl_closure_subst_subset[OF _ M \<delta>, of _ T] M_supset
|
|
timpl_closure_set_is_timpl_closure_union[of "M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>" T]
|
|
timpl_closure_set_is_timpl_closure_union[of M T]
|
|
by auto
|
|
|
|
lemma timpl_closure_set_Union:
|
|
"timpl_closure_set (\<Union>Ms) T = (\<Union>M \<in> Ms. timpl_closure_set M T)"
|
|
using timpl_closure_set_is_timpl_closure_union[of "\<Union>Ms" T]
|
|
timpl_closure_set_is_timpl_closure_union[of _ T]
|
|
by force
|
|
|
|
lemma timpl_closure_set_Union_subst_set:
|
|
assumes "s \<in> timpl_closure_set (\<Union>{M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> | \<delta>. P \<delta>}) T"
|
|
shows "\<exists>\<delta>. P \<delta> \<and> s \<in> timpl_closure_set (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>) T"
|
|
using assms timpl_closure_set_is_timpl_closure_union[of "(\<Union>{M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> | \<delta>. P \<delta>})" T]
|
|
timpl_closure_set_is_timpl_closure_union[of _ T]
|
|
by blast
|
|
|
|
lemma timpl_closure_set_Union_subst_singleton:
|
|
assumes "s \<in> timpl_closure_set {t \<cdot> \<delta> | \<delta>. P \<delta>} T"
|
|
shows "\<exists>\<delta>. P \<delta> \<and> s \<in> timpl_closure_set {t \<cdot> \<delta>} T"
|
|
using assms timpl_closure_set_is_timpl_closure_union[of "{t \<cdot> \<delta> |\<delta>. P \<delta>}" T]
|
|
timpl_closureton_is_timpl_closure[of _ T]
|
|
by fast
|
|
|
|
lemma timpl_closure'_inv:
|
|
assumes "(s, t) \<in> timpl_closure' TI"
|
|
shows "(\<exists>x. s = Var x \<and> t = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> 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) \<in> TI" "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u"
|
|
using timpl_closure'_step_inv[OF step.hyps(2)] by blast
|
|
show ?case using step.IH
|
|
proof
|
|
assume "\<exists>x. s = Var x \<and> t = Var x"
|
|
thus ?case using step.hyps(2) term_variants_pred_inv_Var ab by fastforce
|
|
next
|
|
assume "\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T"
|
|
then obtain f g S T where st: "s = Fun f S" "t = Fun g T" "length S = length T" by moura
|
|
thus ?case
|
|
using ab step.hyps(2) term_variants_pred_inv'[of "(\<lambda>_. [])(Abs a := [Abs b])" g T u]
|
|
by auto
|
|
qed
|
|
qed
|
|
|
|
lemma timpl_closure'_inv':
|
|
assumes "(s, t) \<in> timpl_closure' TI"
|
|
shows "(\<exists>x. s = Var x \<and> t = Var x) \<or>
|
|
(\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T \<and>
|
|
(\<forall>i < length T. (S ! i, T ! i) \<in> timpl_closure' TI) \<and>
|
|
(f \<noteq> g \<longrightarrow> is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> TI\<^sup>+))"
|
|
(is "?A s t \<or> ?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) \<in> TI" "term_variants_pred ((\<lambda>_. [])(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)\<^sup>*)"
|
|
then obtain f g S T where st:
|
|
"s = Fun f S" "t = Fun g T" "length S = length T"
|
|
"\<And>i. i < length T \<Longrightarrow> (S ! i, T ! i) \<in> (timpl_closure'_step TI)\<^sup>*"
|
|
"f \<noteq> g \<Longrightarrow> is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> TI\<^sup>+"
|
|
by moura
|
|
obtain h U where u:
|
|
"u = Fun h U" "length T = length U"
|
|
"\<And>i. i < length T \<Longrightarrow> term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (T ! i) (U ! i)"
|
|
"g \<noteq> h \<Longrightarrow> is_Abs g \<and> is_Abs h \<and> (the_Abs g, the_Abs h) \<in> TI\<^sup>+"
|
|
using ab(2) st(2) r_into_trancl[OF ab(1)]
|
|
term_variants_pred_inv'(1,2,3,4)[of "(\<lambda>_. [])(Abs a := [Abs b])" g T u]
|
|
term_variants_pred_inv'(5)[of "(\<lambda>_. [])(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) \<in> (timpl_closure'_step TI)\<^sup>*" 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 \<and> is_Abs h \<and> (the_Abs f, the_Abs h) \<in> TI\<^sup>+" when fh: "f \<noteq> 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) \<in> timpl_closure' TI"
|
|
shows "length S = length T"
|
|
and "\<And>i. i < length T \<Longrightarrow> (S ! i, T ! i) \<in> timpl_closure' TI"
|
|
and "f \<noteq> g \<Longrightarrow> is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> TI\<^sup>+"
|
|
using assms timpl_closure'_inv' by auto
|
|
|
|
lemma timpl_closure_Fun_inv:
|
|
assumes "s \<in> timpl_closure (Fun f T) TI"
|
|
shows "\<exists>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 \<in> timpl_closure (Fun f T) TI"
|
|
shows "length S = length T"
|
|
and "\<And>i. i < length S \<Longrightarrow> S ! i \<in> timpl_closure (T ! i) TI"
|
|
and "f \<noteq> g \<Longrightarrow> is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> TI\<^sup>+"
|
|
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 \<notin> timpl_closure (Var x) TI"
|
|
using timpl_closure_Var_inv by fast
|
|
|
|
lemma timpl_closure_Var_not_Fun[simp]:
|
|
"Var x \<notin> 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\<^sub>t\<^sub>r\<^sub>m m"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (timpl_closure m TI)"
|
|
proof
|
|
fix t assume "t \<in> timpl_closure m TI"
|
|
thus "wf\<^sub>t\<^sub>r\<^sub>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\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
|
|
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (timpl_closure_set M TI)"
|
|
proof
|
|
fix t assume "t \<in> timpl_closure_set M TI"
|
|
then obtain m where "t \<in> timpl_closure m TI" "m \<in> M" "wf\<^sub>t\<^sub>r\<^sub>m m"
|
|
using M timpl_closure_set_is_timpl_closure_union by blast
|
|
thus "wf\<^sub>t\<^sub>r\<^sub>m t" using timpl_closure_wf_trms by blast
|
|
qed
|
|
|
|
lemma timpl_closure_Fu_inv:
|
|
assumes "t \<in> timpl_closure (Fun (Fu f) T) TI"
|
|
shows "\<exists>S. length S = length T \<and> t = Fun (Fu f) S"
|
|
using assms
|
|
proof (induction t rule: timpl_closure.induct)
|
|
case (TI u a b s)
|
|
then obtain U where U: "length U = length T" "u = Fun (Fu f) U"
|
|
by moura
|
|
hence *: "term_variants_pred ((\<lambda>_. [])(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 \<in> timpl_closure t TI"
|
|
shows "\<exists>S. length S = length T \<and> 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 \<noteq> g \<Longrightarrow> Abs a = g \<and> 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 \<in> timpl_closure s TI"
|
|
and "\<forall>f \<in> funs_term t. \<not>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 \<in> timpl_closure_set FP TI"
|
|
and "\<forall>f \<in> funs_term t. \<not>is_Abs f"
|
|
shows "t \<in> FP"
|
|
using assms timpl_closure_no_Abs_eq unfolding timpl_closure_set_def by blast
|
|
|
|
lemma timpl_closure_funs_term_subset:
|
|
"\<Union>(funs_term ` (timpl_closure t TI)) \<subseteq> funs_term t \<union> Abs ` snd ` TI"
|
|
(is "?A \<subseteq> ?B \<union> ?C")
|
|
proof
|
|
fix f assume "f \<in> ?A"
|
|
then obtain s where "s \<in> timpl_closure t TI" "f \<in> funs_term s" by moura
|
|
thus "f \<in> ?B \<union> ?C"
|
|
proof (induction s rule: timpl_closure.induct)
|
|
case (TI u a b s)
|
|
have "Abs b \<in> 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:
|
|
"\<Union>(funs_term ` (timpl_closure_set FP TI)) \<subseteq> \<Union>(funs_term ` FP) \<union> 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 \<equiv> \<lambda>a. Fun (Abs a) []"
|
|
assumes OCC1: "\<forall>t \<in> FP. \<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> f \<in> Abs ` OCC"
|
|
and OCC2: "snd ` TI \<subseteq> OCC"
|
|
shows "\<forall>t \<in> timpl_closure_set FP TI. \<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> f \<in> Abs ` OCC" (is ?A)
|
|
and "\<forall>t \<in> absc ` OCC. \<forall>(a,b) \<in> TI. \<forall>s \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle>. s \<in> absc ` OCC" (is ?B)
|
|
proof -
|
|
let ?F = "\<Union>(funs_term ` FP)"
|
|
let ?G = "Abs ` snd ` TI"
|
|
|
|
show ?A
|
|
proof (intro ballI impI)
|
|
fix t f assume t: "t \<in> timpl_closure_set FP TI" and f: "f \<in> funs_term t" "is_Abs f"
|
|
hence "f \<in> ?F \<or> f \<in> ?G" using timpl_closure_set_funs_term_subset[of FP TI] by auto
|
|
thus "f \<in> Abs ` OCC"
|
|
proof
|
|
assume "f \<in> ?F" thus ?thesis using OCC1 f(2) by fast
|
|
next
|
|
assume "f \<in> ?G" thus ?thesis using OCC2 by auto
|
|
qed
|
|
qed
|
|
|
|
{ fix s t a b
|
|
assume t: "t \<in> absc ` OCC"
|
|
and ab: "(a, b) \<in> TI"
|
|
and s: "s \<in> set \<langle>a --\<guillemotright> b\<rangle>\<langle>t\<rangle>"
|
|
obtain c where c: "t = absc c" "c \<in> OCC" using t by moura
|
|
hence "s = absc b \<or> s = absc c"
|
|
using ab s timpl_apply_const'[of c a b] unfolding absc_def by auto
|
|
moreover have "b \<in> OCC" using ab OCC2 by auto
|
|
ultimately have "s \<in> 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) prot_terms" and t::"('fun,'atom,'sets) prot_term"
|
|
assumes "M \<turnstile>\<^sub>c t"
|
|
and "s \<in> timpl_closure t TI"
|
|
shows "timpl_closure_set M TI \<turnstile>\<^sub>c s"
|
|
using assms
|
|
proof (induction t arbitrary: s rule: intruder_synth_induct)
|
|
case (AxiomC t)
|
|
hence "s \<in> timpl_closure_set M TI"
|
|
using timpl_closure_set_is_timpl_closure_union[of M TI]
|
|
by blast
|
|
thus ?case by simp
|
|
next
|
|
case (ComposeC T f)
|
|
obtain g S where s: "s = Fun g S"
|
|
using timpl_closure_Fun_inv[OF ComposeC.prems] by moura
|
|
hence s':
|
|
"f = g" "length S = length T"
|
|
"\<And>i. i < length S \<Longrightarrow> S ! i \<in> 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 \<turnstile>\<^sub>c u" when u: "u \<in> 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) prot_terms" and t::"('fun,'atom,'sets) prot_term"
|
|
assumes "timpl_closure_set M TI \<turnstile>\<^sub>c t"
|
|
and "s \<in> timpl_closure t TI"
|
|
shows "timpl_closure_set M TI \<turnstile>\<^sub>c s"
|
|
by (metis intruder_synth_timpl_closure_set[OF assms] timpl_closure_set_idem)
|
|
|
|
lemma timpl_closure_set_absc_subset_in:
|
|
defines "absc \<equiv> \<lambda>a. Fun (Abs a) []"
|
|
assumes A: "timpl_closure_set (absc ` A) TI \<subseteq> absc ` A"
|
|
and a: "a \<in> A" "(a,b) \<in> TI\<^sup>+"
|
|
shows "b \<in> A"
|
|
proof -
|
|
have "timpl_closure (absc a) (TI\<^sup>+) \<subseteq> 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 "[]" "[]" "(\<lambda>_. [])(Abs a := [Abs b])" "Abs b" "Abs a"]
|
|
unfolding absc_def by auto
|
|
qed
|
|
|
|
|
|
subsection \<open>Composition-only Intruder Deduction Modulo Term Implication Closure of the Intruder Knowledge\<close>
|
|
context stateful_protocol_model
|
|
begin
|
|
|
|
fun in_trancl where
|
|
"in_trancl TI a b = (
|
|
if (a,b) \<in> set TI then True
|
|
else list_ex (\<lambda>(c,d). c = a \<and> in_trancl (removeAll (c,d) TI) d b) TI)"
|
|
|
|
definition in_rtrancl where
|
|
"in_rtrancl TI a b \<equiv> a = b \<or> 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 \<or> (is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> set TI)) \<and>
|
|
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 \<or> (is_Abs f \<and> is_Abs g \<and> in_trancl TI (the_Abs f) (the_Abs g))) \<and>
|
|
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 \<or> (is_Abs f \<and> is_Abs g \<and>
|
|
((the_Abs f, the_Abs g) \<in> set TI \<or>
|
|
(the_Abs g, the_Abs f) \<in> set TI \<or>
|
|
(\<exists>ti \<in> set TI. (the_Abs f, snd ti) \<in> set TI \<and> (the_Abs g, snd ti) \<in> set TI)))) \<and>
|
|
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 (\<lambda>t. timpls_transformable_to TI t (Fun f T)) M) \<or>
|
|
(public f \<and> length T = arity f \<and> 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 (\<lambda>t. timpls_transformable_to' TI t (Fun f T)) M) \<or>
|
|
(public f \<and> length T = arity f \<and> 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 \<in> M)"
|
|
| "intruder_synth_mod_eq_timpls M TI (Fun f T) = (
|
|
(\<exists>t \<in> M. equal_mod_timpls TI t (Fun f T)) \<or>
|
|
(public f \<and> length T = arity f \<and> list_all (intruder_synth_mod_eq_timpls M TI) T))"
|
|
|
|
definition analyzed_closed_mod_timpls where
|
|
"analyzed_closed_mod_timpls M TI \<equiv>
|
|
let f = list_all (intruder_synth_mod_timpls M TI);
|
|
g = \<lambda>t. if f (fst (Ana t)) then f (snd (Ana t))
|
|
else \<forall>s \<in> comp_timpl_closure {t} (set TI). case Ana s of (K,R) \<Rightarrow> f K \<longrightarrow> f R
|
|
in list_all g M"
|
|
|
|
definition analyzed_closed_mod_timpls' where
|
|
"analyzed_closed_mod_timpls' M TI \<equiv>
|
|
let f = list_all (intruder_synth_mod_timpls' M TI);
|
|
g = \<lambda>t. if f (fst (Ana t)) then f (snd (Ana t))
|
|
else \<forall>s \<in> comp_timpl_closure {t} (set TI). case Ana s of (K,R) \<Rightarrow> f K \<longrightarrow> f R
|
|
in list_all g M"
|
|
(* Alternative definition (allows for computing the closures beforehand which may be useful) *)
|
|
definition analyzed_closed_mod_timpls_alt where
|
|
"analyzed_closed_mod_timpls_alt M TI timpl_cl_witness \<equiv>
|
|
let f = \<lambda>R. \<forall>r \<in> set R. intruder_synth_mod_timpls M TI r;
|
|
N = {t \<in> set M. f (fst (Ana t))};
|
|
N' = set M - N
|
|
in (\<forall>t \<in> N. f (snd (Ana t))) \<and>
|
|
(N' \<noteq> {} \<longrightarrow> (N' \<union> (\<Union>x\<in>timpl_cl_witness. \<Union>(a,b)\<in>set TI. set \<langle>a --\<guillemotright> b\<rangle>\<langle>x\<rangle>) \<subseteq> timpl_cl_witness)) \<and>
|
|
(\<forall>s \<in> timpl_cl_witness. case Ana s of (K,R) \<Rightarrow> f K \<longrightarrow> f R)"
|
|
|
|
lemma in_trancl_closure_iff_in_trancl_fun:
|
|
"(a,b) \<in> (set TI)\<^sup>+ \<longleftrightarrow> in_trancl TI a b" (is "?A TI a b \<longleftrightarrow> ?B TI a b")
|
|
proof
|
|
show "?A TI a b \<Longrightarrow> ?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) thus ?case using in_trancl.simps
|
|
by (smt Bex_set case_prodE case_prodI member_remove prod.sel(2) remove_code(1))
|
|
qed
|
|
qed (metis in_trancl.simps)
|
|
|
|
show "?B TI a b \<Longrightarrow> ?A TI a b"
|
|
proof (induction TI a b rule: in_trancl.induct)
|
|
case (1 TI a b)
|
|
let ?P = "\<lambda>TI a b c d. in_trancl (List.removeAll (c,d) TI) d b"
|
|
have *: "\<exists>(c,d) \<in> set TI. c = a \<and> ?P TI a b c d" when "(a,b) \<notin> 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) \<in> set TI")
|
|
case False
|
|
hence "\<exists>(c,d) \<in> set TI. c = a \<and> ?P TI a b c d" using * by blast
|
|
then obtain d where d: "(a,d) \<in> set TI" "?P TI a b a d" by blast
|
|
have "(d,b) \<in> (set (removeAll (a,d) TI))\<^sup>+" using "1.IH"[OF False d(1)] d(2) by blast
|
|
moreover have "set (removeAll (a,d) TI) \<subseteq> set TI" by simp
|
|
ultimately have "(d,b) \<in> (set TI)\<^sup>+" 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) \<in> (set TI)\<^sup>* \<longleftrightarrow> 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 \<subseteq> 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 \<Longrightarrow> t = Var x" (is "?A \<Longrightarrow> ?C")
|
|
"equal_mod_timpls TI t (Var x) \<Longrightarrow> t = Var x" (is "?B \<Longrightarrow> ?C")
|
|
proof -
|
|
show "?A \<Longrightarrow> ?C" by (cases t) auto
|
|
show "?B \<Longrightarrow> ?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 "\<And>i. i < length T \<Longrightarrow> equal_mod_timpls TI (T ! i) (S ! i)"
|
|
and "f \<noteq> g \<Longrightarrow> (is_Abs f \<and> is_Abs g \<and> (
|
|
(the_Abs f, the_Abs g) \<in> set TI \<or> (the_Abs g, the_Abs f) \<in> set TI \<or>
|
|
(\<exists>ti \<in> set TI. (the_Abs f, snd ti) \<in> set TI \<and>
|
|
(the_Abs g, snd ti) \<in> 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 "\<And>i. i < length T \<Longrightarrow> equal_mod_timpls TI (T ! i) (args t ! i)"
|
|
and "f \<noteq> the_Fun t \<Longrightarrow> (is_Abs f \<and> is_Abs (the_Fun t) \<and> (
|
|
(the_Abs f, the_Abs (the_Fun t)) \<in> set TI \<or>
|
|
(the_Abs (the_Fun t), the_Abs f) \<in> set TI \<or>
|
|
(\<exists>ti \<in> set TI. (the_Abs f, snd ti) \<in> set TI \<and>
|
|
(the_Abs (the_Fun t), snd ti) \<in> set TI)))"
|
|
and "\<not>is_Abs f \<Longrightarrow> 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) prot_fun, 'd) term" and a b::"'c set"
|
|
defines "P \<equiv> (\<lambda>_. [])(Abs a := [Abs b])"
|
|
assumes st: "term_variants_pred P s t"
|
|
and ab: "(a,b) \<in> 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 \<subseteq> 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 \<or> (is_Abs f \<and> is_Abs g \<and> ((the_Abs f, the_Abs g) \<in> set TI \<or>
|
|
(the_Abs g, the_Abs f) \<in> set TI \<or>
|
|
(\<exists>ti \<in> set TI. (the_Abs f, snd ti) \<in> set TI \<and>
|
|
(the_Abs g, snd ti) \<in> set TI)))"
|
|
"list_all2 (equal_mod_timpls 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) equal_mod_timpls.simps(2) set_rev_mp)
|
|
qed auto
|
|
|
|
lemma equal_mod_timpls_refl_minus_eq:
|
|
"equal_mod_timpls TI s t \<longleftrightarrow> equal_mod_timpls (filter (\<lambda>(a,b). a \<noteq> b) TI) s t"
|
|
(is "?A \<longleftrightarrow> ?B")
|
|
proof
|
|
show ?A when ?B using that equal_mod_timpls_mono[of "filter (\<lambda>(a,b). a \<noteq> 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' \<equiv> filter (\<lambda>(a,b). a \<noteq> b) TI"
|
|
|
|
let ?P = "\<lambda>X Y. f = g \<or> (is_Abs f \<and> is_Abs g \<and> ((the_Abs f, the_Abs g) \<in> set X \<or>
|
|
(the_Abs g, the_Abs f) \<in> set X \<or> (\<exists>ti \<in> set Y.
|
|
(the_Abs f, snd ti) \<in> set X \<and> (the_Abs g, snd ti) \<in> 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 \<Longrightarrow> t = Var x" (is "?A \<Longrightarrow> ?C")
|
|
"timpls_transformable_to TI t (Var x) \<Longrightarrow> t = Var x" (is "?B \<Longrightarrow> ?C")
|
|
"timpls_transformable_to' TI (Var x) t \<Longrightarrow> t = Var x" (is "?A' \<Longrightarrow> ?C")
|
|
"timpls_transformable_to' TI t (Var x) \<Longrightarrow> t = Var x" (is "?B' \<Longrightarrow> ?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 "\<And>i. i < length T \<Longrightarrow> timpls_transformable_to TI (T ! i) (S ! i)"
|
|
and "f \<noteq> g \<Longrightarrow> (is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> 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 "\<And>i. i < length T \<Longrightarrow> timpls_transformable_to' TI (T ! i) (S ! i)"
|
|
and "f \<noteq> g \<Longrightarrow> (is_Abs f \<and> is_Abs g \<and> 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 "\<And>i. i < length T \<Longrightarrow> timpls_transformable_to TI (T ! i) (args t ! i)"
|
|
and "f \<noteq> the_Fun t \<Longrightarrow> (
|
|
is_Abs f \<and> is_Abs (the_Fun t) \<and> (the_Abs f, the_Abs (the_Fun t)) \<in> set TI)"
|
|
and "\<not>is_Abs f \<Longrightarrow> 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 "\<And>i. i < length T \<Longrightarrow> timpls_transformable_to' TI (T ! i) (args t ! i)"
|
|
and "f \<noteq> the_Fun t \<Longrightarrow> (
|
|
is_Abs f \<and> is_Abs (the_Fun t) \<and> in_trancl TI (the_Abs f) (the_Abs (the_Fun t)))"
|
|
and "\<not>is_Abs f \<Longrightarrow> 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::"(('b, 'c, 'a) prot_fun, 'd) term"
|
|
shows "timpls_transformable_to TI s t \<Longrightarrow> size s = size t" (is "?A \<Longrightarrow> ?C")
|
|
and "timpls_transformable_to' TI s t \<Longrightarrow> size s = size t" (is "?B \<Longrightarrow> ?C")
|
|
proof -
|
|
have *: "size_list size T = size_list size S"
|
|
when "length T = length S" "\<And>i. i < length T \<Longrightarrow> size (T ! i) = size (S ! i)"
|
|
for S T::"(('b, 'c, 'a) prot_fun, 'd) 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" "\<And>i. i < length T \<Longrightarrow> 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" "\<And>i. i < length T \<Longrightarrow> 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) prot_fun, 'd) term" and a b::"'c set"
|
|
defines "P \<equiv> (\<lambda>_. [])(Abs a := [Abs b])"
|
|
assumes st: "term_variants_pred P s t"
|
|
and ab: "(a,b) \<in> 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) prot_fun, 'd) term" and a b::"'c set"
|
|
defines "P \<equiv> (\<lambda>_. [])(Abs a := [Abs b])"
|
|
assumes st: "term_variants_pred P s t"
|
|
and ab: "(a,b) \<in> (set TI)\<^sup>+"
|
|
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: "\<forall>(a,b) \<in> (set TI)\<^sup>+. a \<noteq> b \<longrightarrow> (a,b) \<in> 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"
|
|
"\<And>i. i < length T \<Longrightarrow> timpls_transformable_to TI (T ! i) (S ! i)"
|
|
"f \<noteq> g \<Longrightarrow> is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> set TI"
|
|
using timpls_transformable_to_inv'[OF Fun.prems(1)] TI_trancl by moura
|
|
|
|
obtain h U where u:
|
|
"u = Fun h U" "length S = length U"
|
|
"\<And>i. i < length S \<Longrightarrow> timpls_transformable_to TI (S ! i) (U ! i)"
|
|
"g \<noteq> h \<Longrightarrow> is_Abs g \<and> is_Abs h \<and> (the_Abs g, the_Abs h) \<in> set TI"
|
|
using timpls_transformable_to_inv'[OF Fun.prems(2)[unfolded t(1)]] TI_trancl by moura
|
|
|
|
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) \<in> set TI"
|
|
when "(the_Abs f, the_Abs g) \<in> set TI" "(the_Abs g, the_Abs h) \<in> set TI"
|
|
"f \<noteq> 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 \<and> is_Abs h \<and> (the_Abs f, the_Abs h) \<in> set TI"
|
|
when "f \<noteq> 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"
|
|
"\<And>i. i < length T \<Longrightarrow> timpls_transformable_to' TI (T ! i) (S ! i)"
|
|
"f \<noteq> g \<Longrightarrow> is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> (set TI)\<^sup>+"
|
|
using timpls_transformable_to'_inv'[OF Fun.prems(1)] 0 by moura
|
|
|
|
obtain h U where u:
|
|
"u = Fun h U" "length S = length U"
|
|
"\<And>i. i < length S \<Longrightarrow> timpls_transformable_to' TI (S ! i) (U ! i)"
|
|
"g \<noteq> h \<Longrightarrow> is_Abs g \<and> is_Abs h \<and> (the_Abs g, the_Abs h) \<in> (set TI)\<^sup>+"
|
|
using timpls_transformable_to'_inv'[OF Fun.prems(2)[unfolded t(1)]] 0 by moura
|
|
|
|
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) \<in> (set TI)\<^sup>+"
|
|
when "(the_Abs f, the_Abs g) \<in> (set TI)\<^sup>+" "(the_Abs g, the_Abs h) \<in> (set TI)\<^sup>+"
|
|
using that by simp
|
|
hence "is_Abs f \<and> is_Abs h \<and> (the_Abs f, the_Abs h) \<in> (set TI)\<^sup>+"
|
|
when "f \<noteq> 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 \<subseteq> 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 \<or> (is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> 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 \<subseteq> 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 \<or> (is_Abs f \<and> is_Abs g \<and> 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 \<longleftrightarrow> timpls_transformable_to (filter (\<lambda>(a,b). a \<noteq> b) TI) s t"
|
|
(is "?A \<longleftrightarrow> ?B")
|
|
proof
|
|
let ?TI' = "\<lambda>TI. filter (\<lambda>(a,b). a \<noteq> 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 \<or> (is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> set TI)"
|
|
"list_all2 (timpls_transformable_to TI) T S"
|
|
using "2.prems" by simp_all
|
|
|
|
have "f = g \<or> (is_Abs f \<and> is_Abs g \<and> (the_Abs f, the_Abs g) \<in> 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) \<in> (set TI)\<^sup>+. a \<noteq> b}"
|
|
shows "timpls_transformable_to TI' s t \<longleftrightarrow> t \<in> timpl_closure s (set TI)" (is "?A s t \<longleftrightarrow> ?B s t")
|
|
proof
|
|
show "?A s t \<Longrightarrow> ?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" "\<forall>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) \<in> 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 \<in> 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 \<or> (\<exists>a b. (a, b) \<in> (set TI')\<^sup>+ \<and> f = Abs a \<and> 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 \<Longrightarrow> ?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) \<in> set TI'" when cd: "(c,d) \<in> (set TI')\<^sup>+" "c \<noteq> d" for c d
|
|
proof -
|
|
let ?cl = "\<lambda>X. {(a,b) \<in> X\<^sup>+. a \<noteq> 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 \<longleftrightarrow> t \<in> timpl_closure s (set TI)" (is "?A s t \<longleftrightarrow> ?B s t")
|
|
proof
|
|
show "?A s t \<Longrightarrow> ?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" "\<forall>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) \<in> 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 \<in> 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 \<or> (\<exists>a b. (a, b) \<in> (set TI)\<^sup>+ \<and> f = Abs a \<and> 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 \<Longrightarrow> ?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) \<in> TI\<^sup>+. a \<noteq> b}"
|
|
shows "equal_mod_timpls TI' s t \<longleftrightarrow> (\<exists>u. u \<in> timpl_closure s TI \<and> u \<in> timpl_closure t TI)"
|
|
(is "?A s t \<longleftrightarrow> ?B s t")
|
|
proof
|
|
show "?A s t \<Longrightarrow> ?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" "\<forall>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: "\<exists>u. (T ! i, u) \<in> timpl_closure' TI \<and> (S ! i, u) \<in> 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 "\<exists>u. u \<in> timpl_closure (T ! i) TI \<and> u \<in> 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 = "\<lambda>G. f = g \<or> (\<exists>a b. (a, b) \<in> G \<and> f = Abs a \<and> g = Abs b) \<or>
|
|
(\<exists>a b. (a, b) \<in> G \<and> f = Abs b \<and> g = Abs a) \<or>
|
|
(\<exists>a b c. (a, c) \<in> G \<and> (b, c) \<in> G \<and> f = Abs a \<and> 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\<^sup>+)" unfolding prems by blast
|
|
hence "?P (rtrancl TI)" by (metis (no_types, lifting) trancl_into_rtrancl)
|
|
hence 5: "f = g \<or> (\<exists>a b c. (a, c) \<in> TI\<^sup>* \<and> (b, c) \<in> TI\<^sup>* \<and> f = Abs a \<and> 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 \<in> timpl_closure s TI" "u \<in> timpl_closure t TI"
|
|
using B by moura
|
|
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"
|
|
"\<And>i. i < length U \<Longrightarrow> U ! i \<in> timpl_closure (S ! i) TI"
|
|
"g \<noteq> f \<Longrightarrow> is_Abs g \<and> is_Abs f \<and> (the_Abs g, the_Abs f) \<in> TI\<^sup>+"
|
|
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"
|
|
"\<And>i. i < length U \<Longrightarrow> U ! i \<in> timpl_closure (T ! i) TI"
|
|
"h \<noteq> f \<Longrightarrow> is_Abs h \<and> is_Abs f \<and> (the_Abs h, the_Abs f) \<in> TI\<^sup>+"
|
|
using Fun.prems(2) timpl_closure_Fun_inv'[of f U _ _ TI]
|
|
by (cases t) auto
|
|
|
|
have g: "(the_Abs g, the_Abs f) \<in> set TI'" "is_Abs f" "is_Abs g" when neq_f: "g \<noteq> 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 \<noteq> the_Abs f" using neq_f by simp
|
|
thus "(the_Abs g, the_Abs f) \<in> 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) \<in> set TI'" "is_Abs f" "is_Abs h" when neq_f: "h \<noteq> 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 \<noteq> the_Abs f" using neq_f by simp
|
|
thus "(the_Abs h, the_Abs f) \<in> 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
|
|
|
|
(* lemma equal_mod_timpls_iff_ex_in_timpl_closure':
|
|
"equal_mod_timpls (TI\<^sup>+) s t \<longleftrightarrow> (\<exists>u. u \<in> timpl_closure s TI \<and> u \<in> timpl_closure t TI)"
|
|
using equal_mod_timpls_iff_ex_in_timpl_closure equal_mod_timpls_refl_minus_eq
|
|
by blast *)
|
|
|
|
context
|
|
begin
|
|
private inductive timpls_transformable_to_pred where
|
|
Var: "timpls_transformable_to_pred A (Var x) (Var x)"
|
|
| Fun: "\<lbrakk>\<not>is_Abs f; length T = length S;
|
|
\<And>i. i < length T \<Longrightarrow> timpls_transformable_to_pred A (T ! i) (S ! i)\<rbrakk>
|
|
\<Longrightarrow> timpls_transformable_to_pred A (Fun f T) (Fun f S)"
|
|
| Abs: "b \<in> A \<Longrightarrow> 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 "\<And>i. i < length T \<Longrightarrow> timpls_transformable_to_pred A (T ! i) (args t ! i)"
|
|
and "\<not>is_Abs f \<Longrightarrow> f = the_Fun t"
|
|
and "is_Abs f \<Longrightarrow> (is_Abs (the_Fun t) \<and> the_Abs (the_Fun t) \<in> A)"
|
|
using assms by (auto elim!: timpls_transformable_to_pred.cases[of A])
|
|
|
|
private lemma timpls_transformable_to_pred_finite_aux1:
|
|
assumes f: "\<not>is_Abs f"
|
|
shows "{s. timpls_transformable_to_pred A (Fun f T) s} \<subseteq>
|
|
(\<lambda>S. Fun f S) ` {S. length T = length S \<and>
|
|
(\<forall>s \<in> set S. \<exists>t \<in> set T. timpls_transformable_to_pred A t s)}"
|
|
(is "?B \<subseteq> ?C")
|
|
proof
|
|
fix s assume s: "s \<in> ?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" "\<And>i. i < length T \<Longrightarrow> 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 "\<forall>s\<in>set S. \<exists>t\<in>set T. timpls_transformable_to_pred A t s" using S(2,3) in_set_conv_nth by metis
|
|
thus "s \<in> ?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} \<subseteq> (\<lambda>b. Fun (Abs b) []) ` A" (is "?B \<subseteq> ?C")
|
|
proof
|
|
fix s assume s: "s \<in> ?B"
|
|
hence *: "timpls_transformable_to_pred A (Fun (Abs a) []) s" by blast
|
|
|
|
obtain b where b: "s = Fun (Abs b) []" "b \<in> A"
|
|
using timpls_transformable_to_pred_inv[OF *] unfolding the_Abs_def is_Abs_def by auto
|
|
thus "s \<in> ?C" by blast
|
|
qed
|
|
|
|
private lemma timpls_transformable_to_pred_finite:
|
|
fixes t::"(('fun,'atom,'sets) prot_fun, 'a) term"
|
|
assumes A: "finite A"
|
|
and t: "wf\<^sub>t\<^sub>r\<^sub>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) 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 \<in> 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} \<subseteq> (\<lambda>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\<^sub>t\<^sub>r\<^sub>m t" "\<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> the_Abs f \<in> A"
|
|
shows "timpls_transformable_to_pred (A \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+) t s"
|
|
using s t
|
|
proof (induction rule: timpls_transformable_to.induct)
|
|
case (2 TI f T g S)
|
|
let ?A = "A \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+"
|
|
|
|
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 "\<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> the_Abs f \<in> A" when t: "t \<in> 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 \<in> ?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 moura
|
|
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) \<in> (set TI)\<^sup>+"
|
|
using 0(3) in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
|
|
unfolding is_Abs_def the_Abs_def by fastforce
|
|
hence "a \<in> ?A" "b \<in> ?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\<^sub>t\<^sub>r\<^sub>m t" "\<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> the_Abs f \<in> A"
|
|
shows "timpls_transformable_to_pred (A \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+) t s"
|
|
using s t
|
|
proof (induction rule: timpls_transformable_to.induct)
|
|
case (2 TI f T g S)
|
|
let ?A = "A \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+"
|
|
|
|
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 "\<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> the_Abs f \<in> A" when t: "t \<in> 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 \<in> ?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 moura
|
|
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) \<in> (set TI)\<^sup>+"
|
|
using 0(3) in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
|
|
unfolding is_Abs_def the_Abs_def by fastforce
|
|
hence "a \<in> ?A" "b \<in> ?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\<^sub>t\<^sub>r\<^sub>m t" "\<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> the_Abs f \<in> A"
|
|
shows "timpls_transformable_to_pred (A \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+) t s"
|
|
using s t
|
|
proof (induction rule: equal_mod_timpls.induct)
|
|
case (2 TI f T g S)
|
|
let ?A = "A \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+"
|
|
|
|
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 "\<forall>f \<in> funs_term t. is_Abs f \<longrightarrow> the_Abs f \<in> A" when t: "t \<in> 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 \<in> ?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 moura
|
|
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) \<in> (set TI)\<^sup>+ \<or> (b, a) \<in> (set TI)\<^sup>+ \<or>
|
|
(\<exists>ti \<in> set TI. (a, snd ti) \<in> (set TI)\<^sup>+ \<and> (b, snd ti) \<in> (set TI)\<^sup>+)"
|
|
using 0(3) in_trancl_closure_iff_in_trancl_fun[of _ _ TI]
|
|
unfolding is_Abs_def the_Abs_def by fastforce
|
|
hence "a \<in> ?A" "b \<in> ?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\<^sub>t\<^sub>r\<^sub>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 \<in> funs_term t. is_Abs f} \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+"
|
|
|
|
have 0: "finite ?A" by auto
|
|
|
|
have 1: "{s. timpls_transformable_to TI t s} \<subseteq> {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} \<subseteq> {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\<^sub>t\<^sub>r\<^sub>m t"
|
|
shows "finite {s. equal_mod_timpls TI t s}"
|
|
proof -
|
|
let ?A = "the_Abs ` {f \<in> funs_term t. is_Abs f} \<union> fst ` (set TI)\<^sup>+ \<union> snd ` (set TI)\<^sup>+"
|
|
|
|
have 0: "finite ?A" by auto
|
|
|
|
have 1: "{s. equal_mod_timpls TI t s} \<subseteq> {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) prot_fun, 'a) term" and TI TI'
|
|
assumes "set TI' = {(a,b) \<in> (set TI)\<^sup>+. a \<noteq> b}"
|
|
shows "intruder_synth_mod_timpls M TI' t \<longleftrightarrow> timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c t"
|
|
(is "?C t \<longleftrightarrow> ?D t")
|
|
proof -
|
|
have *: "(\<exists>m \<in> M. timpls_transformable_to TI' m t) \<longleftrightarrow> t \<in> timpl_closure_set M (set TI)"
|
|
when "set TI' = {(a,b) \<in> (set TI)\<^sup>+. a \<noteq> b}"
|
|
for M TI TI' and t::"(('fun, 'atom, 'sets) 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 \<longleftrightarrow> ?D t"
|
|
proof
|
|
show "?C t \<Longrightarrow> ?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 \<in> 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 "\<exists>m \<in> 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 "\<not>(list_ex (\<lambda>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 \<Longrightarrow> ?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) prot_fun, 'a) term" and TI
|
|
shows "intruder_synth_mod_timpls' M TI t \<longleftrightarrow> timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c t"
|
|
(is "?A t \<longleftrightarrow> ?B t")
|
|
proof -
|
|
have *: "(\<exists>m \<in> M. timpls_transformable_to' TI m t) \<longleftrightarrow> t \<in> timpl_closure_set M (set TI)"
|
|
for M TI and t::"(('fun, 'atom, 'sets) 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 \<longleftrightarrow> ?B t"
|
|
proof
|
|
show "?A t \<Longrightarrow> ?B t"
|
|
proof (induction t arbitrary: M TI rule: intruder_synth_mod_timpls'.induct)
|
|
case (1 M TI x)
|
|
hence "Var x \<in> 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 "\<exists>m \<in> 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 \<Longrightarrow> ?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) prot_fun, 'a) term" and TI
|
|
defines "cl \<equiv> \<lambda>TI. {(a,b) \<in> TI\<^sup>+. a \<noteq> b}"
|
|
shows (* "set TI' = (set TI)\<^sup>+ \<Longrightarrow>
|
|
intruder_synth_mod_eq_timpls M TI' t \<longleftrightarrow>
|
|
(\<exists>s \<in> timpl_closure t (set TI). timpl_closure_set M (set TI) \<turnstile>\<^sub>c s)"
|
|
(is "?P TI TI' \<Longrightarrow> ?A t \<longleftrightarrow> ?B t")
|
|
and *) "set TI' = {(a,b) \<in> (set TI)\<^sup>+. a \<noteq> b} \<Longrightarrow>
|
|
intruder_synth_mod_eq_timpls M TI' t \<longleftrightarrow>
|
|
(\<exists>s \<in> timpl_closure t (set TI). timpl_closure_set M (set TI) \<turnstile>\<^sub>c s)"
|
|
(is "?Q TI TI' \<Longrightarrow> ?C t \<longleftrightarrow> ?D t")
|
|
proof -
|
|
(* have *: "(\<exists>m \<in> M. equal_mod_timpls TI' m t) \<longleftrightarrow>
|
|
(\<exists>s \<in> timpl_closure t (set TI). s \<in> timpl_closure_set M (set TI))"
|
|
when P: "?P TI TI'"
|
|
for M TI TI' and t::"(('fun, 'atom, 'sets) prot_fun, 'a) term"
|
|
using equal_mod_timpls_iff_ex_in_timpl_closure'[OF P]
|
|
timpl_closure_set_is_timpl_closure_union[of M "set TI"]
|
|
timpl_closure_set_timpls_trancl_eq[of M "set TI"]
|
|
by blast *)
|
|
|
|
have **: "(\<exists>m \<in> M. equal_mod_timpls TI' m t) \<longleftrightarrow>
|
|
(\<exists>s \<in> timpl_closure t (set TI). s \<in> timpl_closure_set M (set TI))"
|
|
when Q: "?Q TI TI'"
|
|
for M TI TI' and t::"(('fun, 'atom, 'sets) 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 "?A t \<longleftrightarrow> ?B t" when P: "?P TI TI'"
|
|
proof
|
|
show "?A t \<Longrightarrow> ?B t"
|
|
proof (induction t arbitrary: M TI rule: intruder_synth_mod_eq_timpls.induct)
|
|
case (1 M TI x)
|
|
hence "Var x \<in> timpl_closure_set M TI" "Var x \<in> timpl_closure (Var x) TI"
|
|
using timpl_closure.FP unfolding timpl_closure_set_def by auto
|
|
thus ?case by force
|
|
next
|
|
case (2 M TI f T)
|
|
show ?case
|
|
proof (cases "\<exists>m \<in> M. equal_mod_timpls (TI\<^sup>+) m (Fun f T)")
|
|
case True thus ?thesis
|
|
using "2.prems" *[of M TI "Fun f T"] intruder_synth.AxiomC[of _ "timpl_closure_set M TI"]
|
|
by blast
|
|
next
|
|
case False
|
|
hence f: "public f" "length T = arity f" "list_all (intruder_synth_mod_eq_timpls M (TI\<^sup>+)) T"
|
|
using "2.prems" by force+
|
|
|
|
let ?sy = "intruder_synth (timpl_closure_set M TI)"
|
|
|
|
have IH: "\<exists>u \<in> timpl_closure (T ! i) TI. ?sy u"
|
|
when i: "i < length T" for i
|
|
using "2.IH"[of _ M TI] f(3) nth_mem[OF i]
|
|
unfolding list_all_iff by blast
|
|
|
|
define S where "S \<equiv> map (\<lambda>u. SOME v. v \<in> timpl_closure u TI \<and> ?sy v) T"
|
|
|
|
have S1: "length T = length S"
|
|
unfolding S_def by simp
|
|
|
|
have S2: "S ! i \<in> timpl_closure (T ! i) TI"
|
|
"timpl_closure_set M TI \<turnstile>\<^sub>c S ! i"
|
|
when i: "i < length S" for i
|
|
using i IH someI_ex[of "\<lambda>v. v \<in> timpl_closure (T ! i) TI \<and> ?sy v"]
|
|
unfolding S_def by auto
|
|
|
|
have "Fun f S \<in> timpl_closure (Fun f T) TI"
|
|
using timpl_closure_FunI[of T S 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 "?A t" when B: "?B t"
|
|
proof -
|
|
obtain s where "timpl_closure_set M TI \<turnstile>\<^sub>c s" "s \<in> timpl_closure t TI"
|
|
using B by moura
|
|
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 TI] timpl_closure_Var_inv[of s _ TI]
|
|
note 2 = *[of M TI]
|
|
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"
|
|
"\<forall>i < length T. T ! i \<in> timpl_closure (S ! i) TI"
|
|
"g \<noteq> f \<Longrightarrow> is_Abs g \<and> is_Abs f \<and> (the_Abs g, the_Abs f) \<in> TI\<^sup>+"
|
|
using ComposeC.prems(1) timpl_closure'_inv'[of t "Fun f T" TI]
|
|
timpl_closure_is_timpl_closure'[of _ _ TI]
|
|
by fastforce
|
|
|
|
have IH: "intruder_synth_mod_eq_timpls M (TI\<^sup>+) u" when u: "u \<in> 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\<^sup>+)" S]
|
|
intruder_synth_mod_eq_timpls.simps(2)[of M "TI\<^sup>+" 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 *)
|
|
|
|
show "?C t \<longleftrightarrow> ?D t" when Q: "?Q TI TI'"
|
|
proof
|
|
show "?C t \<Longrightarrow> ?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 \<in> timpl_closure_set M (set TI)" "Var x \<in> 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 "\<exists>m \<in> 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: "\<exists>u \<in> 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 \<equiv> map (\<lambda>u. SOME v. v \<in> timpl_closure u (set TI) \<and> ?sy v) T"
|
|
|
|
have S1: "length T = length S"
|
|
unfolding S_def by simp
|
|
|
|
have S2: "S ! i \<in> timpl_closure (T ! i) (set TI)"
|
|
"timpl_closure_set M (set TI) \<turnstile>\<^sub>c S ! i"
|
|
when i: "i < length S" for i
|
|
using i IH someI_ex[of "\<lambda>v. v \<in> timpl_closure (T ! i) (set TI) \<and> ?sy v"]
|
|
unfolding S_def by auto
|
|
|
|
have "Fun f S \<in> 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) \<turnstile>\<^sub>c s" "s \<in> timpl_closure t (set TI)"
|
|
using D by moura
|
|
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"
|
|
"\<forall>i < length T. T ! i \<in> timpl_closure (S ! i) (set TI)"
|
|
"g \<noteq> f \<Longrightarrow> is_Abs g \<and> is_Abs f \<and> (the_Abs g, the_Abs f) \<in> (set TI)\<^sup>+"
|
|
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 \<in> 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\<^sub>t\<^sub>r\<^sub>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 \<times> 'sets set) list"
|
|
assumes M_finite: "finite M"
|
|
and M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>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 \<times> 'sets set) list"
|
|
assumes M_finite: "finite M"
|
|
and M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>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) prot_terms"
|
|
assumes f: "arity\<^sub>f f = length T" "arity\<^sub>f f > 0" "Ana\<^sub>f f = (K, R)"
|
|
and i: "i < length R"
|
|
and M: "timpl_closure_set M TI \<turnstile>\<^sub>c T ! (R ! i)"
|
|
and m: "Fun (Fu f) T \<in> M"
|
|
and t: "Fun (Fu f) S \<in> timpl_closure (Fun (Fu f) T) TI"
|
|
shows "timpl_closure_set M TI \<turnstile>\<^sub>c S ! (R ! i)"
|
|
proof -
|
|
have "R ! i < length T" using i Ana\<^sub>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) prot_terms"
|
|
assumes M: "\<forall>s \<in> set (snd (Ana m)). timpl_closure_set M TI \<turnstile>\<^sub>c s"
|
|
and m: "m \<in> M"
|
|
and t: "t \<in> timpl_closure m TI"
|
|
and s: "s \<in> set (snd (Ana t))"
|
|
shows "timpl_closure_set M TI \<turnstile>\<^sub>c s"
|
|
proof -
|
|
obtain f S K N where fS: "t = Fun (Fu f) S" "arity\<^sub>f f = length S" "0 < arity\<^sub>f f"
|
|
and Ana_f: "Ana\<^sub>f f = (K, N)"
|
|
and Ana_t: "Ana t = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>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 moura
|
|
hence Ana_m: "Ana m = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>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 (\<lambda>i. S ! i) N"]
|
|
by auto
|
|
hence "timpl_closure_set M TI \<turnstile>\<^sub>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) prot_term list"
|
|
assumes TI': "set TI' = {(a,b) \<in> (set TI)\<^sup>+. a \<noteq> b}"
|
|
and M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
|
|
shows "analyzed_closed_mod_timpls M TI' \<longleftrightarrow> analyzed (timpl_closure_set (set M) (set TI))"
|
|
(is "?A \<longleftrightarrow> ?B")
|
|
proof
|
|
let ?C = "\<forall>t \<in> timpl_closure_set (set M) (set TI).
|
|
analyzed_in t (timpl_closure_set (set M) (set TI))"
|
|
|
|
let ?P = "\<lambda>T. \<forall>t \<in> set T. timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c t"
|
|
let ?Q = "\<lambda>t. \<forall>s \<in> comp_timpl_closure {t} (set TI'). case Ana s of (K, R) \<Rightarrow> ?P K \<longrightarrow> ?P R"
|
|
|
|
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 {t} (set TI') = timpl_closure_set {t} (set TI)"
|
|
when t: "t \<in> set M" "wf\<^sub>t\<^sub>r\<^sub>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}" TI']
|
|
unfolding TI'[symmetric]
|
|
by blast
|
|
hence 3: "comp_timpl_closure {t} (set TI') \<subseteq> timpl_closure_set (set M) (set TI)"
|
|
when t: "t \<in> set M" "wf\<^sub>t\<^sub>r\<^sub>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[OF TI']
|
|
list_all_iff Let_def
|
|
proof (intro ballI)
|
|
fix t assume t: "t \<in> set M"
|
|
show "if ?P (fst (Ana t)) then ?P (snd (Ana t)) 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 \<in> timpl_closure_set (set M) (set TI)"
|
|
and s: "s \<in> set T"
|
|
and Ana_t: "Ana t = (K, T)"
|
|
and K: "\<forall>k \<in> set K. timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c k"
|
|
|
|
obtain m where m: "m \<in> set M" "t \<in> timpl_closure m (set TI)"
|
|
using timpl_closure_set_is_timpl_closure_union t by moura
|
|
|
|
show "timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c s"
|
|
proof (cases "\<forall>k \<in> set (fst (Ana m)). timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c k")
|
|
case True
|
|
hence *: "\<forall>r \<in> set (snd (Ana m)). timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>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
|
|
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
|
|
hence "?Q m"
|
|
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 auto
|
|
moreover 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
|
|
ultimately show ?thesis
|
|
using m(2) K s Ana_t
|
|
unfolding Let_def by auto
|
|
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) prot_term list"
|
|
assumes M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
|
|
shows "analyzed_closed_mod_timpls' M TI \<longleftrightarrow> analyzed (timpl_closure_set (set M) (set TI))"
|
|
(is "?A \<longleftrightarrow> ?B")
|
|
proof
|
|
let ?C = "\<forall>t \<in> timpl_closure_set (set M) (set TI). analyzed_in t (timpl_closure_set (set M) (set TI))"
|
|
|
|
let ?P = "\<lambda>T. \<forall>t \<in> set T. timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c t"
|
|
let ?Q = "\<lambda>t. \<forall>s \<in> comp_timpl_closure {t} (set TI). case Ana s of (K, R) \<Rightarrow> ?P K \<longrightarrow> ?P R"
|
|
|
|
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 \<in> set M" "wf\<^sub>t\<^sub>r\<^sub>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) \<subseteq> timpl_closure_set (set M) (set TI)"
|
|
when t: "t \<in> set M" "wf\<^sub>t\<^sub>r\<^sub>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 \<in> set M"
|
|
show "if ?P (fst (Ana t)) then ?P (snd (Ana t)) 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 \<in> timpl_closure_set (set M) (set TI)"
|
|
and s: "s \<in> set T"
|
|
and Ana_t: "Ana t = (K, T)"
|
|
and K: "\<forall>k \<in> set K. timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c k"
|
|
|
|
obtain m where m: "m \<in> set M" "t \<in> timpl_closure m (set TI)"
|
|
using timpl_closure_set_is_timpl_closure_union t by moura
|
|
|
|
show "timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c s"
|
|
proof (cases "\<forall>k \<in> set (fst (Ana m)). timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>c k")
|
|
case True
|
|
hence *: "\<forall>r \<in> set (snd (Ana m)). timpl_closure_set (set M) (set TI) \<turnstile>\<^sub>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
|
|
hence "?Q m"
|
|
using m(1) A
|
|
unfolding analyzed_closed_mod_timpls'_def
|
|
intruder_synth_mod_timpls'_is_synth_timpl_closure_set
|
|
list_all_iff Let_def
|
|
by auto
|
|
moreover 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
|
|
ultimately show ?thesis
|
|
using m(2) K s Ana_t
|
|
unfolding Let_def by auto
|
|
qed
|
|
qed
|
|
thus ?B when A: ?A using A analyzed_is_all_analyzed_in by metis
|
|
qed
|
|
|
|
end
|
|
|
|
end
|
|
|
|
end
|