Stateful_Protocol_Compositi.../Stateful_Protocol_Compositi.../Stateful_Strands.thy

1757 lines
116 KiB
Plaintext

(*
(C) Copyright Andreas Viktor Hess, DTU, 2018-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: Stateful_Strands.thy
Author: Andreas Viktor Hess, DTU
*)
section \<open>Stateful Strands\<close>
theory Stateful_Strands
imports Strands_and_Constraints
begin
subsection \<open>Stateful Constraints\<close>
datatype (funs\<^sub>s\<^sub>s\<^sub>t\<^sub>p: 'a, vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p: 'b) stateful_strand_step =
Send (the_msg: "('a,'b) term") ("send\<langle>_\<rangle>" 80)
| Receive (the_msg: "('a,'b) term") ("receive\<langle>_\<rangle>" 80)
| Equality (the_check: poscheckvariant) (the_lhs: "('a,'b) term") (the_rhs: "('a,'b) term")
("\<langle>_: _ \<doteq> _\<rangle>" [80,80])
| Insert (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term") ("insert\<langle>_,_\<rangle>" 80)
| Delete (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term") ("delete\<langle>_,_\<rangle>" 80)
| InSet (the_check: poscheckvariant) (the_elem_term: "('a,'b) term") (the_set_term: "('a,'b) term")
("\<langle>_: _ \<in> _\<rangle>" [80,80])
| NegChecks (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p: "'b list")
(the_eqs: "(('a,'b) term \<times> ('a,'b) term) list")
(the_ins: "(('a,'b) term \<times> ('a,'b) term) list")
("\<forall>_\<langle>\<or>\<noteq>: _ \<or>\<notin>: _\<rangle>" [80,80])
where
"bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Send _) = []"
| "bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Receive _) = []"
| "bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Equality _ _ _) = []"
| "bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Insert _ _) = []"
| "bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Delete _ _) = []"
| "bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (InSet _ _ _) = []"
type_synonym ('a,'b) stateful_strand = "('a,'b) stateful_strand_step list"
type_synonym ('a,'b) dbstatelist = "(('a,'b) term \<times> ('a,'b) term) list"
type_synonym ('a,'b) dbstate = "(('a,'b) term \<times> ('a,'b) term) set"
abbreviation
"is_Assignment x \<equiv> (is_Equality x \<or> is_InSet x) \<and> the_check x = Assign"
abbreviation
"is_Check x \<equiv> ((is_Equality x \<or> is_InSet x) \<and> the_check x = Check) \<or> is_NegChecks x"
abbreviation
"is_Update x \<equiv> is_Insert x \<or> is_Delete x"
abbreviation InSet_select ("select\<langle>_,_\<rangle>") where "select\<langle>t,s\<rangle> \<equiv> InSet Assign t s"
abbreviation InSet_check ("\<langle>_ in _\<rangle>") where "\<langle>t in s\<rangle> \<equiv> InSet Check t s"
abbreviation Equality_assign ("\<langle>_ := _\<rangle>") where "\<langle>t := s\<rangle> \<equiv> Equality Assign t s"
abbreviation Equality_check ("\<langle>_ == _\<rangle>") where "\<langle>t == s\<rangle> \<equiv> Equality Check t s"
abbreviation NegChecks_Inequality1 ("\<langle>_ != _\<rangle>") where
"\<langle>t != s\<rangle> \<equiv> NegChecks [] [(t,s)] []"
abbreviation NegChecks_Inequality2 ("\<forall>_\<langle>_ != _\<rangle>") where
"\<forall>x\<langle>t != s\<rangle> \<equiv> NegChecks [x] [(t,s)] []"
abbreviation NegChecks_Inequality3 ("\<forall>_,_\<langle>_ != _\<rangle>") where
"\<forall>x,y\<langle>t != s\<rangle> \<equiv> NegChecks [x,y] [(t,s)] []"
abbreviation NegChecks_Inequality4 ("\<forall>_,_,_\<langle>_ != _\<rangle>") where
"\<forall>x,y,z\<langle>t != s\<rangle> \<equiv> NegChecks [x,y,z] [(t,s)] []"
abbreviation NegChecks_NotInSet1 ("\<langle>_ not in _\<rangle>") where
"\<langle>t not in s\<rangle> \<equiv> NegChecks [] [] [(t,s)]"
abbreviation NegChecks_NotInSet2 ("\<forall>_\<langle>_ not in _\<rangle>") where
"\<forall>x\<langle>t not in s\<rangle> \<equiv> NegChecks [x] [] [(t,s)]"
abbreviation NegChecks_NotInSet3 ("\<forall>_,_\<langle>_ not in _\<rangle>") where
"\<forall>x,y\<langle>t not in s\<rangle> \<equiv> NegChecks [x,y] [] [(t,s)]"
abbreviation NegChecks_NotInSet4 ("\<forall>_,_,_\<langle>_ not in _\<rangle>") where
"\<forall>x,y,z\<langle>t not in s\<rangle> \<equiv> NegChecks [x,y,z] [] [(t,s)]"
fun trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p where
"trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Send t) = {t}"
| "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Receive t) = {t}"
| "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Equality _ t t') = {t,t'}"
| "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Insert t t') = {t,t'}"
| "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Delete t t') = {t,t'}"
| "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (InSet _ t t') = {t,t'}"
| "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (NegChecks _ F F') = trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F'"
definition trms\<^sub>s\<^sub>s\<^sub>t where "trms\<^sub>s\<^sub>s\<^sub>t S \<equiv> \<Union>(trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p ` set S)"
declare trms\<^sub>s\<^sub>s\<^sub>t_def[simp]
fun trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p where
"trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Send t) = [t]"
| "trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Receive t) = [t]"
| "trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Equality _ t t') = [t,t']"
| "trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Insert t t') = [t,t']"
| "trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Delete t t') = [t,t']"
| "trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (InSet _ t t') = [t,t']"
| "trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (NegChecks _ F F') = concat (map (\<lambda>(t,t'). [t,t']) (F@F'))"
definition trms_list\<^sub>s\<^sub>s\<^sub>t where "trms_list\<^sub>s\<^sub>s\<^sub>t S \<equiv> remdups (concat (map trms_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p S))"
definition ik\<^sub>s\<^sub>s\<^sub>t where "ik\<^sub>s\<^sub>s\<^sub>t A \<equiv> {t. Receive t \<in> set A}"
definition bvars\<^sub>s\<^sub>s\<^sub>t::"('a,'b) stateful_strand \<Rightarrow> 'b set" where
"bvars\<^sub>s\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map (set \<circ> bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p) S))"
fun fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p::"('a,'b) stateful_strand_step \<Rightarrow> 'b set" where
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Send t) = fv t"
| "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Receive t) = fv t"
| "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Equality _ t t') = fv t \<union> fv t'"
| "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Insert t t') = fv t \<union> fv t'"
| "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Delete t t') = fv t \<union> fv t'"
| "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (InSet _ t t') = fv t \<union> fv t'"
| "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (NegChecks X F F') = fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' - set X"
definition fv\<^sub>s\<^sub>s\<^sub>t::"('a,'b) stateful_strand \<Rightarrow> 'b set" where
"fv\<^sub>s\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p S))"
fun fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p where
"fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (send\<langle>t\<rangle>) = fv_list t"
| "fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (receive\<langle>t\<rangle>) = fv_list t"
| "fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>_: t \<doteq> s\<rangle>) = fv_list t@fv_list s"
| "fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (insert\<langle>t,s\<rangle>) = fv_list t@fv_list s"
| "fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (delete\<langle>t,s\<rangle>) = fv_list t@fv_list s"
| "fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>_: t \<in> s\<rangle>) = fv_list t@fv_list s"
| "fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle>) = filter (\<lambda>x. x \<notin> set X) (fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F@F'))"
definition fv_list\<^sub>s\<^sub>s\<^sub>t where
"fv_list\<^sub>s\<^sub>s\<^sub>t S \<equiv> remdups (concat (map fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p S))"
declare bvars\<^sub>s\<^sub>s\<^sub>t_def[simp]
declare fv\<^sub>s\<^sub>s\<^sub>t_def[simp]
definition vars\<^sub>s\<^sub>s\<^sub>t::"('a,'b) stateful_strand \<Rightarrow> 'b set" where
"vars\<^sub>s\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p S))"
abbreviation wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p::"('a,'b) stateful_strand_step \<Rightarrow> 'b set" where
"wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x \<equiv>
case x of
NegChecks _ _ _ \<Rightarrow> {}
| Equality Check _ _ \<Rightarrow> {}
| InSet Check _ _ \<Rightarrow> {}
| Delete _ _ \<Rightarrow> {}
| _ \<Rightarrow> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x"
definition wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t::"('a,'b) stateful_strand \<Rightarrow> 'b set" where
"wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p S))"
abbreviation wfvarsoccs\<^sub>s\<^sub>s\<^sub>t\<^sub>p where
"wfvarsoccs\<^sub>s\<^sub>s\<^sub>t\<^sub>p x \<equiv>
case x of
Send t \<Rightarrow> fv t
| Equality Assign s t \<Rightarrow> fv s
| InSet Assign s t \<Rightarrow> fv s \<union> fv t
| _ \<Rightarrow> {}"
definition wfvarsoccs\<^sub>s\<^sub>s\<^sub>t where
"wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map wfvarsoccs\<^sub>s\<^sub>s\<^sub>t\<^sub>p S))"
fun wf'\<^sub>s\<^sub>s\<^sub>t::"'b set \<Rightarrow> ('a,'b) stateful_strand \<Rightarrow> bool" where
"wf'\<^sub>s\<^sub>s\<^sub>t V [] = True"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (Receive t#S) = (fv t \<subseteq> V \<and> wf'\<^sub>s\<^sub>s\<^sub>t V S)"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (Send t#S) = wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t) S"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (Equality Assign t t'#S) = (fv t' \<subseteq> V \<and> wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t) S)"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (Equality Check _ _#S) = wf'\<^sub>s\<^sub>s\<^sub>t V S"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (Insert t s#S) = (fv t \<subseteq> V \<and> fv s \<subseteq> V \<and> wf'\<^sub>s\<^sub>s\<^sub>t V S)"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (Delete _ _#S) = wf'\<^sub>s\<^sub>s\<^sub>t V S"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (InSet Assign t s#S) = wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> fv s) S"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (InSet Check _ _#S) = wf'\<^sub>s\<^sub>s\<^sub>t V S"
| "wf'\<^sub>s\<^sub>s\<^sub>t V (NegChecks _ _ _#S) = wf'\<^sub>s\<^sub>s\<^sub>t V S"
abbreviation "wf\<^sub>s\<^sub>s\<^sub>t S \<equiv> wf'\<^sub>s\<^sub>s\<^sub>t {} S \<and> fv\<^sub>s\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>s\<^sub>t S = {}"
fun subst_apply_stateful_strand_step::
"('a,'b) stateful_strand_step \<Rightarrow> ('a,'b) subst \<Rightarrow> ('a,'b) stateful_strand_step"
(infix "\<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p" 51) where
"send\<langle>t\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = send\<langle>t \<cdot> \<theta>\<rangle>"
| "receive\<langle>t\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = receive\<langle>t \<cdot> \<theta>\<rangle>"
| "\<langle>a: t \<doteq> s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<langle>a: (t \<cdot> \<theta>) \<doteq> (s \<cdot> \<theta>)\<rangle>"
| "\<langle>a: t \<in> s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<langle>a: (t \<cdot> \<theta>) \<in> (s \<cdot> \<theta>)\<rangle>"
| "insert\<langle>t,s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = insert\<langle>t \<cdot> \<theta>, s \<cdot> \<theta>\<rangle>"
| "delete\<langle>t,s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = delete\<langle>t \<cdot> \<theta>, s \<cdot> \<theta>\<rangle>"
| "\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<forall>X\<langle>\<or>\<noteq>: (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<or>\<notin>: (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>)\<rangle>"
definition subst_apply_stateful_strand::
"('a,'b) stateful_strand \<Rightarrow> ('a,'b) subst \<Rightarrow> ('a,'b) stateful_strand"
(infix "\<cdot>\<^sub>s\<^sub>s\<^sub>t" 51) where
"S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta> \<equiv> map (\<lambda>x. x \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) S"
fun dbupd\<^sub>s\<^sub>s\<^sub>t::"('f,'v) stateful_strand \<Rightarrow> ('f,'v) subst \<Rightarrow> ('f,'v) dbstate \<Rightarrow> ('f,'v) dbstate"
where
"dbupd\<^sub>s\<^sub>s\<^sub>t [] I D = D"
| "dbupd\<^sub>s\<^sub>s\<^sub>t (Insert t s#A) I D = dbupd\<^sub>s\<^sub>s\<^sub>t A I (insert ((t,s) \<cdot>\<^sub>p I) D)"
| "dbupd\<^sub>s\<^sub>s\<^sub>t (Delete t s#A) I D = dbupd\<^sub>s\<^sub>s\<^sub>t A I (D - {((t,s) \<cdot>\<^sub>p I)})"
| "dbupd\<^sub>s\<^sub>s\<^sub>t (_#A) I D = dbupd\<^sub>s\<^sub>s\<^sub>t A I D"
fun db'\<^sub>s\<^sub>s\<^sub>t::"('f,'v) stateful_strand \<Rightarrow> ('f,'v) subst \<Rightarrow> ('f,'v) dbstatelist \<Rightarrow> ('f,'v) dbstatelist"
where
"db'\<^sub>s\<^sub>s\<^sub>t [] I D = D"
| "db'\<^sub>s\<^sub>s\<^sub>t (Insert t s#A) I D = db'\<^sub>s\<^sub>s\<^sub>t A I (List.insert ((t,s) \<cdot>\<^sub>p I) D)"
| "db'\<^sub>s\<^sub>s\<^sub>t (Delete t s#A) I D = db'\<^sub>s\<^sub>s\<^sub>t A I (List.removeAll ((t,s) \<cdot>\<^sub>p I) D)"
| "db'\<^sub>s\<^sub>s\<^sub>t (_#A) I D = db'\<^sub>s\<^sub>s\<^sub>t A I D"
definition db\<^sub>s\<^sub>s\<^sub>t where
"db\<^sub>s\<^sub>s\<^sub>t S I \<equiv> db'\<^sub>s\<^sub>s\<^sub>t S I []"
fun setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p where
"setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Insert t s) = {(t,s)}"
| "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Delete t s) = {(t,s)}"
| "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (InSet _ t s) = {(t,s)}"
| "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (NegChecks _ _ F') = set F'"
| "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p _ = {}"
text \<open>The set-operations of a stateful strand\<close>
definition setops\<^sub>s\<^sub>s\<^sub>t where
"setops\<^sub>s\<^sub>s\<^sub>t S \<equiv> \<Union>(setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p ` set S)"
fun setops_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p where
"setops_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Insert t s) = [(t,s)]"
| "setops_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (Delete t s) = [(t,s)]"
| "setops_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (InSet _ t s) = [(t,s)]"
| "setops_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p (NegChecks _ _ F') = F'"
| "setops_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p _ = []"
text \<open>The set-operations of a stateful strand (list variant)\<close>
definition setops_list\<^sub>s\<^sub>s\<^sub>t where
"setops_list\<^sub>s\<^sub>s\<^sub>t S \<equiv> remdups (concat (map setops_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p S))"
subsection \<open>Small Lemmata\<close>
lemma trms_list\<^sub>s\<^sub>s\<^sub>t_is_trms\<^sub>s\<^sub>s\<^sub>t: "trms\<^sub>s\<^sub>s\<^sub>t S = set (trms_list\<^sub>s\<^sub>s\<^sub>t S)"
unfolding trms\<^sub>s\<^sub>t_def trms_list\<^sub>s\<^sub>s\<^sub>t_def
proof (induction S)
case (Cons x S) thus ?case by (cases x) auto
qed simp
lemma setops_list\<^sub>s\<^sub>s\<^sub>t_is_setops\<^sub>s\<^sub>s\<^sub>t: "setops\<^sub>s\<^sub>s\<^sub>t S = set (setops_list\<^sub>s\<^sub>s\<^sub>t S)"
unfolding setops\<^sub>s\<^sub>s\<^sub>t_def setops_list\<^sub>s\<^sub>s\<^sub>t_def
proof (induction S)
case (Cons x S) thus ?case by (cases x) auto
qed simp
lemma fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p: "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p a = set (fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p a)"
proof (cases a)
case (NegChecks X F G) thus ?thesis
using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_append[of F G] fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_append[of F G]
fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_is_fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s[of "F@G"]
by auto
qed (simp_all add: fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_is_fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s fv_list_is_fv)
lemma fv_list\<^sub>s\<^sub>s\<^sub>t_is_fv\<^sub>s\<^sub>s\<^sub>t: "fv\<^sub>s\<^sub>s\<^sub>t S = set (fv_list\<^sub>s\<^sub>s\<^sub>t S)"
unfolding fv\<^sub>s\<^sub>s\<^sub>t_def fv_list\<^sub>s\<^sub>s\<^sub>t_def by (induct S) (simp_all add: fv_list\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p)
lemma trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite[simp]: "finite (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p x)"
by (cases x) auto
lemma trms\<^sub>s\<^sub>s\<^sub>t_finite[simp]: "finite (trms\<^sub>s\<^sub>s\<^sub>t S)"
using trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite unfolding trms\<^sub>s\<^sub>s\<^sub>t_def by (induct S) auto
lemma vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite[simp]: "finite (vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x)"
by (cases x) auto
lemma vars\<^sub>s\<^sub>s\<^sub>t_finite[simp]: "finite (vars\<^sub>s\<^sub>s\<^sub>t S)"
using vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite unfolding vars\<^sub>s\<^sub>s\<^sub>t_def by (induct S) auto
lemma fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite[simp]: "finite (fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p x)"
by (cases x) auto
lemma fv\<^sub>s\<^sub>s\<^sub>t_finite[simp]: "finite (fv\<^sub>s\<^sub>s\<^sub>t S)"
using fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite unfolding fv\<^sub>s\<^sub>s\<^sub>t_def by (induct S) auto
lemma bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite[simp]: "finite (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x))"
by (rule finite_set)
lemma bvars\<^sub>s\<^sub>s\<^sub>t_finite[simp]: "finite (bvars\<^sub>s\<^sub>s\<^sub>t S)"
using bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_finite unfolding bvars\<^sub>s\<^sub>s\<^sub>t_def by (induct S) auto
lemma subst_sst_nil[simp]: "[] \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta> = []"
by (simp add: subst_apply_stateful_strand_def)
lemma db\<^sub>s\<^sub>s\<^sub>t_nil[simp]: "db\<^sub>s\<^sub>s\<^sub>t [] \<I> = []"
by (simp add: db\<^sub>s\<^sub>s\<^sub>t_def)
lemma ik\<^sub>s\<^sub>s\<^sub>t_nil[simp]: "ik\<^sub>s\<^sub>s\<^sub>t [] = {}"
by (simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
lemma ik\<^sub>s\<^sub>s\<^sub>t_append[simp]: "ik\<^sub>s\<^sub>s\<^sub>t (A@B) = ik\<^sub>s\<^sub>s\<^sub>t A \<union> ik\<^sub>s\<^sub>s\<^sub>t B"
by (auto simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
lemma ik\<^sub>s\<^sub>s\<^sub>t_subst: "ik\<^sub>s\<^sub>s\<^sub>t (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>) = ik\<^sub>s\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>"
proof (induction A)
case (Cons a A) thus ?case
by (cases a) (auto simp add: ik\<^sub>s\<^sub>s\<^sub>t_def subst_apply_stateful_strand_def)
qed simp
lemma db\<^sub>s\<^sub>s\<^sub>t_set_is_dbupd\<^sub>s\<^sub>s\<^sub>t: "set (db'\<^sub>s\<^sub>s\<^sub>t A I D) = dbupd\<^sub>s\<^sub>s\<^sub>t A I (set D)" (is "?A = ?B")
proof
show "?A \<subseteq> ?B"
proof
fix t s show "(t,s) \<in> ?A \<Longrightarrow> (t,s) \<in> ?B" by (induct rule: db'\<^sub>s\<^sub>s\<^sub>t.induct) auto
qed
show "?B \<subseteq> ?A"
proof
fix t s show "(t,s) \<in> ?B \<Longrightarrow> (t,s) \<in> ?A" by (induct arbitrary: D rule: dbupd\<^sub>s\<^sub>s\<^sub>t.induct) auto
qed
qed
lemma dbupd\<^sub>s\<^sub>s\<^sub>t_no_upd:
assumes "\<forall>a \<in> set A. \<not>is_Insert a \<and> \<not>is_Delete a"
shows "dbupd\<^sub>s\<^sub>s\<^sub>t A I D = D"
using assms
proof (induction A)
case (Cons a A) thus ?case by (cases a) auto
qed simp
lemma db\<^sub>s\<^sub>s\<^sub>t_no_upd:
assumes "\<forall>a \<in> set A. \<not>is_Insert a \<and> \<not>is_Delete a"
shows "db'\<^sub>s\<^sub>s\<^sub>t A I D = D"
using assms
proof (induction A)
case (Cons a A) thus ?case by (cases a) auto
qed simp
lemma db\<^sub>s\<^sub>s\<^sub>t_no_upd_append:
assumes "\<forall>b \<in> set B. \<not>is_Insert b \<and> \<not>is_Delete b"
shows "db'\<^sub>s\<^sub>s\<^sub>t A = db'\<^sub>s\<^sub>s\<^sub>t (A@B)"
using assms
proof (induction A)
case Nil thus ?case by (simp add: db\<^sub>s\<^sub>s\<^sub>t_no_upd)
next
case (Cons a A) thus ?case by (cases a) simp_all
qed
lemma db\<^sub>s\<^sub>s\<^sub>t_append:
"db'\<^sub>s\<^sub>s\<^sub>t (A@B) I D = db'\<^sub>s\<^sub>s\<^sub>t B I (db'\<^sub>s\<^sub>s\<^sub>t A I D)"
proof (induction A arbitrary: D)
case (Cons a A) thus ?case by (cases a) auto
qed simp
lemma db\<^sub>s\<^sub>s\<^sub>t_in_cases:
assumes "(t,s) \<in> set (db'\<^sub>s\<^sub>s\<^sub>t A I D)"
shows "(t,s) \<in> set D \<or> (\<exists>t' s'. insert\<langle>t',s'\<rangle> \<in> set A \<and> t = t' \<cdot> I \<and> s = s' \<cdot> I)"
using assms
proof (induction A arbitrary: D)
case (Cons a A) thus ?case by (cases a) fastforce+
qed simp
lemma db\<^sub>s\<^sub>s\<^sub>t_in_cases':
assumes "(t,s) \<in> set (db'\<^sub>s\<^sub>s\<^sub>t A I D)"
and "(t,s) \<notin> set D"
shows "\<exists>B C t' s'. A = B@insert\<langle>t',s'\<rangle>#C \<and> t = t' \<cdot> I \<and> s = s' \<cdot> I \<and>
(\<forall>t'' s''. delete\<langle>t'',s''\<rangle> \<in> set C \<longrightarrow> t \<noteq> t'' \<cdot> I \<or> s \<noteq> s'' \<cdot> I)"
using assms(1)
proof (induction A rule: List.rev_induct)
case (snoc a A)
note * = snoc db\<^sub>s\<^sub>s\<^sub>t_append[of A "[a]" I D]
thus ?case
proof (cases a)
case (Insert t' s')
thus ?thesis using * by (cases "(t,s) \<in> set (db'\<^sub>s\<^sub>s\<^sub>t A I D)") force+
next
case (Delete t' s')
hence **: "t \<noteq> t' \<cdot> I \<or> s \<noteq> s' \<cdot> I" using * by simp
have "(t,s) \<in> set (db'\<^sub>s\<^sub>s\<^sub>t A I D)" using * Delete by force
then obtain B C u v where B:
"A = B@insert\<langle>u,v\<rangle>#C" "t = u \<cdot> I" "s = v \<cdot> I"
"\<forall>t' s'. delete\<langle>t',s'\<rangle> \<in> set C \<longrightarrow> t \<noteq> t' \<cdot> I \<or> s \<noteq> s' \<cdot> I"
using snoc.IH by moura
have "A@[a] = B@insert\<langle>u,v\<rangle>#(C@[a])"
"\<forall>t' s'. delete\<langle>t',s'\<rangle> \<in> set (C@[a]) \<longrightarrow> t \<noteq> t' \<cdot> I \<or> s \<noteq> s' \<cdot> I"
using B(1,4) Delete ** by auto
thus ?thesis using B(2,3) by blast
qed force+
qed (simp add: assms(2))
lemma db\<^sub>s\<^sub>s\<^sub>t_filter:
"db'\<^sub>s\<^sub>s\<^sub>t A I D = db'\<^sub>s\<^sub>s\<^sub>t (filter is_Update A) I D"
by (induct A I D rule: db'\<^sub>s\<^sub>s\<^sub>t.induct) simp_all
lemma subst_sst_cons: "a#A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta> = (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)#(A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
by (simp add: subst_apply_stateful_strand_def)
lemma subst_sst_snoc: "A@[a] \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta> = (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)@[a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>]"
by (simp add: subst_apply_stateful_strand_def)
lemma subst_sst_append[simp]: "A@B \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta> = (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)@(B \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
by (simp add: subst_apply_stateful_strand_def)
lemma sst_vars_append_subset:
"fv\<^sub>s\<^sub>s\<^sub>t A \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (A@B)" "bvars\<^sub>s\<^sub>s\<^sub>t A \<subseteq> bvars\<^sub>s\<^sub>s\<^sub>t (A@B)"
"fv\<^sub>s\<^sub>s\<^sub>t B \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (A@B)" "bvars\<^sub>s\<^sub>s\<^sub>t B \<subseteq> bvars\<^sub>s\<^sub>s\<^sub>t (A@B)"
by auto
lemma sst_vars_disj_cons[simp]: "fv\<^sub>s\<^sub>s\<^sub>t (a#A) \<inter> bvars\<^sub>s\<^sub>s\<^sub>t (a#A) = {} \<Longrightarrow> fv\<^sub>s\<^sub>s\<^sub>t A \<inter> bvars\<^sub>s\<^sub>s\<^sub>t A = {}"
unfolding fv\<^sub>s\<^sub>s\<^sub>t_def bvars\<^sub>s\<^sub>s\<^sub>t_def by auto
lemma fv\<^sub>s\<^sub>s\<^sub>t_cons_subset[simp]: "fv\<^sub>s\<^sub>s\<^sub>t A \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (a#A)"
by auto
lemma fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases[simp]:
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (send\<langle>t\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>)"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (receive\<langle>t\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>)"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<doteq> s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (insert\<langle>t,s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (delete\<langle>t,s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<in> s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) =
fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) - set X"
by simp_all
lemma vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_cases[simp]:
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (send\<langle>t\<rangle>) = fv t"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (receive\<langle>t\<rangle>) = fv t"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<doteq> s\<rangle>) = fv t \<union> fv s"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (insert\<langle>t,s\<rangle>) = fv t \<union> fv s"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (delete\<langle>t,s\<rangle>) = fv t \<union> fv s"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<in> s\<rangle>) = fv t \<union> fv s"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>) = fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<union> set X" (is ?A)
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: [(t,s)] \<or>\<notin>: []\<rangle>) = fv t \<union> fv s \<union> set X" (is ?B)
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: [] \<or>\<notin>: [(t,s)]\<rangle>) = fv t \<union> fv s \<union> set X" (is ?C)
proof
show ?A ?B ?C by auto
qed simp_all
lemma vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases[simp]:
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (send\<langle>t\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>)"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (receive\<langle>t\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>)"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<doteq> s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (insert\<langle>t,s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (delete\<langle>t,s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<in> s\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = fv (t \<cdot> \<theta>) \<union> fv (s \<cdot> \<theta>)"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) =
fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<union> set X" (is ?A)
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: [(t,s)] \<or>\<notin>: []\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) =
fv (t \<cdot> rm_vars (set X) \<theta>) \<union> fv (s \<cdot> rm_vars (set X) \<theta>) \<union> set X" (is ?B)
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: [] \<or>\<notin>: [(t,s)]\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) =
fv (t \<cdot> rm_vars (set X) \<theta>) \<union> fv (s \<cdot> rm_vars (set X) \<theta>) \<union> set X" (is ?C)
proof
show ?A ?B ?C by auto
qed simp_all
lemma bvars\<^sub>s\<^sub>s\<^sub>t_cons_subset: "bvars\<^sub>s\<^sub>s\<^sub>t A \<subseteq> bvars\<^sub>s\<^sub>s\<^sub>t (a#A)"
by auto
lemma bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst: "bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) = bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a"
by (cases a) auto
lemma bvars\<^sub>s\<^sub>s\<^sub>t_subst: "bvars\<^sub>s\<^sub>s\<^sub>t (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>) = bvars\<^sub>s\<^sub>s\<^sub>t A"
using bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst[of _ \<delta>]
by (induct A) (simp_all add: subst_apply_stateful_strand_def)
lemma bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_set_cases[simp]:
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (send\<langle>t\<rangle>)) = {}"
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (receive\<langle>t\<rangle>)) = {}"
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<doteq> s\<rangle>)) = {}"
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (insert\<langle>t,s\<rangle>)) = {}"
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (delete\<langle>t,s\<rangle>)) = {}"
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>c: t \<in> s\<rangle>)) = {}"
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>)) = set X"
by simp_all
lemma bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegChecks: "\<not>is_NegChecks a \<Longrightarrow> bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a = []"
by (cases a) simp_all
lemma bvars\<^sub>s\<^sub>s\<^sub>t_NegChecks: "bvars\<^sub>s\<^sub>s\<^sub>t A = bvars\<^sub>s\<^sub>s\<^sub>t (filter is_NegChecks A)"
proof (induction A)
case (Cons a A) thus ?case by (cases a) fastforce+
qed simp
lemma vars\<^sub>s\<^sub>s\<^sub>t_append[simp]: "vars\<^sub>s\<^sub>s\<^sub>t (A@B) = vars\<^sub>s\<^sub>s\<^sub>t A \<union> vars\<^sub>s\<^sub>s\<^sub>t B"
by (simp add: vars\<^sub>s\<^sub>s\<^sub>t_def)
lemma vars\<^sub>s\<^sub>s\<^sub>t_Nil[simp]: "vars\<^sub>s\<^sub>s\<^sub>t [] = {}"
by (simp add: vars\<^sub>s\<^sub>s\<^sub>t_def)
lemma vars\<^sub>s\<^sub>s\<^sub>t_Cons: "vars\<^sub>s\<^sub>s\<^sub>t (a#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
by (simp add: vars\<^sub>s\<^sub>s\<^sub>t_def)
lemma fv\<^sub>s\<^sub>s\<^sub>t_Cons: "fv\<^sub>s\<^sub>s\<^sub>t (a#A) = fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<union> fv\<^sub>s\<^sub>s\<^sub>t A"
unfolding fv\<^sub>s\<^sub>s\<^sub>t_def by simp
lemma bvars\<^sub>s\<^sub>s\<^sub>t_Cons: "bvars\<^sub>s\<^sub>s\<^sub>t (a#A) = set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a) \<union> bvars\<^sub>s\<^sub>s\<^sub>t A"
unfolding bvars\<^sub>s\<^sub>s\<^sub>t_def by auto
lemma vars\<^sub>s\<^sub>s\<^sub>t_Cons'[simp]:
"vars\<^sub>s\<^sub>s\<^sub>t (send\<langle>t\<rangle>#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (send\<langle>t\<rangle>) \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
"vars\<^sub>s\<^sub>s\<^sub>t (receive\<langle>t\<rangle>#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (receive\<langle>t\<rangle>) \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
"vars\<^sub>s\<^sub>s\<^sub>t (\<langle>a: t \<doteq> s\<rangle>#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>a: t \<doteq> s\<rangle>) \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
"vars\<^sub>s\<^sub>s\<^sub>t (insert\<langle>t,s\<rangle>#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (insert\<langle>t,s\<rangle>) \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
"vars\<^sub>s\<^sub>s\<^sub>t (delete\<langle>t,s\<rangle>#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (delete\<langle>t,s\<rangle>) \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
"vars\<^sub>s\<^sub>s\<^sub>t (\<langle>a: t \<in> s\<rangle>#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>a: t \<in> s\<rangle>) \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
"vars\<^sub>s\<^sub>s\<^sub>t (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>#A) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>) \<union> vars\<^sub>s\<^sub>s\<^sub>t A"
by (simp_all add: vars\<^sub>s\<^sub>s\<^sub>t_def)
lemma vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p:
fixes x::"('a,'b) stateful_strand_step"
shows "vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x = fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p x \<union> set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x)"
proof (cases x)
case (NegChecks X F G) thus ?thesis by (induct F) force+
qed simp_all
lemma vars\<^sub>s\<^sub>s\<^sub>t_is_fv\<^sub>s\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>s\<^sub>t:
fixes S::"('a,'b) stateful_strand"
shows "vars\<^sub>s\<^sub>s\<^sub>t S = fv\<^sub>s\<^sub>s\<^sub>t S \<union> bvars\<^sub>s\<^sub>s\<^sub>t S"
proof (induction S)
case (Cons x S) thus ?case
using vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p[of x]
by (auto simp add: vars\<^sub>s\<^sub>s\<^sub>t_def)
qed simp
lemma vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegCheck[simp]:
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>) = set X \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G"
by (simp_all add: sup_commute sup_left_commute vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p)
lemma bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegCheck[simp]:
"bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>) = X"
"set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>[]\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>)) = {}"
by simp_all
lemma fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegCheck[simp]:
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>) = fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G - set X"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<forall>[]\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle>) = fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>t != s\<rangle>) = fv t \<union> fv s"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>t not in s\<rangle>) = fv t \<union> fv s"
by simp_all
lemma fv\<^sub>s\<^sub>s\<^sub>t_append[simp]: "fv\<^sub>s\<^sub>s\<^sub>t (A@B) = fv\<^sub>s\<^sub>s\<^sub>t A \<union> fv\<^sub>s\<^sub>s\<^sub>t B"
by simp
lemma bvars\<^sub>s\<^sub>s\<^sub>t_append[simp]: "bvars\<^sub>s\<^sub>s\<^sub>t (A@B) = bvars\<^sub>s\<^sub>s\<^sub>t A \<union> bvars\<^sub>s\<^sub>s\<^sub>t B"
by auto
lemma fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_subterm_trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p:
assumes "x \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p a"
shows "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a)"
using assms var_is_subterm
proof (cases a)
case (NegChecks X F F')
hence "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' - set X" using assms by simp
thus ?thesis using NegChecks var_is_subterm by fastforce
qed force+
lemma fv\<^sub>s\<^sub>s\<^sub>t_is_subterm_trms\<^sub>s\<^sub>s\<^sub>t: "x \<in> fv\<^sub>s\<^sub>s\<^sub>t A \<Longrightarrow> Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t A)"
proof (induction A)
case (Cons a A) thus ?case using fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_subterm_trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p by (cases "x \<in> fv\<^sub>s\<^sub>s\<^sub>t A") auto
qed simp
lemma var_subterm_trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p:
assumes "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a)"
shows "x \<in> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a"
using assms vars_iff_subtermeq
proof (cases a)
case (NegChecks X F F')
hence "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F')" using assms by simp
thus ?thesis using NegChecks vars_iff_subtermeq by force
qed force+
lemma var_subterm_trms\<^sub>s\<^sub>s\<^sub>t_is_vars\<^sub>s\<^sub>s\<^sub>t: "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t A) \<Longrightarrow> x \<in> vars\<^sub>s\<^sub>s\<^sub>t A"
proof (induction A)
case (Cons a A)
show ?case
proof (cases "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t A)")
case True thus ?thesis using Cons.IH by (simp add: vars\<^sub>s\<^sub>s\<^sub>t_def)
next
case False thus ?thesis
using Cons.prems var_subterm_trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_is_vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p
by (fastforce simp add: vars\<^sub>s\<^sub>s\<^sub>t_def)
qed
qed simp
lemma var_trms\<^sub>s\<^sub>s\<^sub>t_is_vars\<^sub>s\<^sub>s\<^sub>t: "Var x \<in> trms\<^sub>s\<^sub>s\<^sub>t A \<Longrightarrow> x \<in> vars\<^sub>s\<^sub>s\<^sub>t A"
by (meson var_subterm_trms\<^sub>s\<^sub>s\<^sub>t_is_vars\<^sub>s\<^sub>s\<^sub>t UN_I term.order_refl)
lemma ik\<^sub>s\<^sub>s\<^sub>t_trms\<^sub>s\<^sub>s\<^sub>t_subset: "ik\<^sub>s\<^sub>s\<^sub>t A \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t A"
by (force simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
lemma var_subterm_ik\<^sub>s\<^sub>s\<^sub>t_is_vars\<^sub>s\<^sub>s\<^sub>t: "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>s\<^sub>t A) \<Longrightarrow> x \<in> vars\<^sub>s\<^sub>s\<^sub>t A"
using var_subterm_trms\<^sub>s\<^sub>s\<^sub>t_is_vars\<^sub>s\<^sub>s\<^sub>t ik\<^sub>s\<^sub>s\<^sub>t_trms\<^sub>s\<^sub>s\<^sub>t_subset by fast
lemma var_subterm_ik\<^sub>s\<^sub>s\<^sub>t_is_fv\<^sub>s\<^sub>s\<^sub>t:
assumes "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>s\<^sub>t A)"
shows "x \<in> fv\<^sub>s\<^sub>s\<^sub>t A"
proof -
obtain t where t: "Receive t \<in> set A" "Var x \<sqsubseteq> t" using assms unfolding ik\<^sub>s\<^sub>s\<^sub>t_def by moura
hence "fv t \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t A" unfolding fv\<^sub>s\<^sub>s\<^sub>t_def by force
thus ?thesis using t(2) by (meson contra_subsetD subterm_is_var)
qed
lemma fv_ik\<^sub>s\<^sub>s\<^sub>t_is_fv\<^sub>s\<^sub>s\<^sub>t:
assumes "x \<in> fv\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>s\<^sub>t A)"
shows "x \<in> fv\<^sub>s\<^sub>s\<^sub>t A"
using var_subterm_ik\<^sub>s\<^sub>s\<^sub>t_is_fv\<^sub>s\<^sub>s\<^sub>t assms var_is_subterm by fastforce
lemma fv_trms\<^sub>s\<^sub>s\<^sub>t_subset:
"fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S) \<subseteq> vars\<^sub>s\<^sub>s\<^sub>t S"
"fv\<^sub>s\<^sub>s\<^sub>t S \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S)"
proof (induction S)
case (Cons x S)
have *: "fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t (x#S)) = fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p x) \<union> fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S)"
"fv\<^sub>s\<^sub>s\<^sub>t (x#S) = fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p x \<union> fv\<^sub>s\<^sub>s\<^sub>t S" "vars\<^sub>s\<^sub>s\<^sub>t (x#S) = vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x \<union> vars\<^sub>s\<^sub>s\<^sub>t S"
unfolding trms\<^sub>s\<^sub>s\<^sub>t_def fv\<^sub>s\<^sub>s\<^sub>t_def vars\<^sub>s\<^sub>s\<^sub>t_def
by auto
{ case 1
show ?case using Cons.IH(1)
proof (cases x)
case (NegChecks X F G)
hence "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p x = trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G"
"vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x = fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<union> set X"
by (simp, meson vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_cases(7))
hence "fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p x) \<subseteq> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x"
using fv_trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_is_fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s[of F] fv_trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_is_fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s[of G]
by auto
thus ?thesis
using Cons.IH(1) *(1,3)
by blast
qed auto
}
{ case 2
show ?case using Cons.IH(2)
proof (cases x)
case (NegChecks X F G)
hence "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p x = trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G"
"fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p x = (fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G) - set X"
by auto
hence "fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p x \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p x)"
using fv_trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_is_fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s[of F] fv_trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_is_fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s[of G]
by auto
thus ?thesis
using Cons.IH(2) *(1,2)
by blast
qed auto
}
qed simp_all
lemma fv_ik_subset_fv_sst'[simp]: "fv\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>s\<^sub>t S) \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
unfolding ik\<^sub>s\<^sub>s\<^sub>t_def by (induct S) auto
lemma fv_ik_subset_vars_sst'[simp]: "fv\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>s\<^sub>t S) \<subseteq> vars\<^sub>s\<^sub>s\<^sub>t S"
using fv_ik_subset_fv_sst' fv_trms\<^sub>s\<^sub>s\<^sub>t_subset by fast
lemma ik\<^sub>s\<^sub>s\<^sub>t_var_is_fv: "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>s\<^sub>t A) \<Longrightarrow> x \<in> fv\<^sub>s\<^sub>s\<^sub>t A"
by (meson fv_ik_subset_fv_sst'[of A] fv_subset_subterms subsetCE term.set_intros(3))
lemma vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases':
assumes x: "x \<in> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
shows "x \<in> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s \<or> x \<in> fv\<^sub>s\<^sub>e\<^sub>t (\<theta> ` vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s)"
using x vars_term_subst[of _ \<theta>] vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_cases(1,2,3,4,5,6) vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(1,2)[of _ \<theta>]
vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(3,6)[of _ _ _ \<theta>] vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(4,5)[of _ _ \<theta>]
proof (cases s)
case (NegChecks X F G)
let ?\<theta>' = "rm_vars (set X) \<theta>"
have "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<theta>') \<or> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<theta>') \<or> x \<in> set X"
using vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(7)[of X F G \<theta>] x NegChecks by simp
hence "x \<in> fv\<^sub>s\<^sub>e\<^sub>t (?\<theta>' ` fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<or> x \<in> fv\<^sub>s\<^sub>e\<^sub>t (?\<theta>' ` fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G) \<or> x \<in> set X"
using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst[of _ ?\<theta>'] by blast
hence "x \<in> fv\<^sub>s\<^sub>e\<^sub>t (\<theta> ` fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<or> x \<in> fv\<^sub>s\<^sub>e\<^sub>t (\<theta> ` fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G) \<or> x \<in> set X"
using rm_vars_fv\<^sub>s\<^sub>e\<^sub>t_subst by fast
thus ?thesis
using NegChecks vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_cases(7)[of X F G]
by auto
qed simp_all
lemma vars\<^sub>s\<^sub>s\<^sub>t_subst_cases:
assumes "x \<in> vars\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
shows "x \<in> vars\<^sub>s\<^sub>s\<^sub>t S \<or> x \<in> fv\<^sub>s\<^sub>e\<^sub>t (\<theta> ` vars\<^sub>s\<^sub>s\<^sub>t S)"
using assms
proof (induction S)
case (Cons s S) thus ?case
proof (cases "x \<in> vars\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)")
case False
note * = subst_sst_cons[of s S \<theta>] vars\<^sub>s\<^sub>s\<^sub>t_Cons[of "s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>" "S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>"] vars\<^sub>s\<^sub>s\<^sub>t_Cons[of s S]
have **: "x \<in> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)" using Cons.prems False * by simp
show ?thesis using vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases'[OF **] * by auto
qed (auto simp add: vars\<^sub>s\<^sub>s\<^sub>t_def)
qed simp
lemma subset_subst_pairs_diff_exists:
fixes \<I>::"('a,'b) subst" and D D'::"('a,'b) dbstate"
shows "\<exists>Di. Di \<subseteq> D \<and> Di \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I> = (D \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>) - D'"
by (metis (no_types, lifting) Diff_subset subset_image_iff)
lemma subset_subst_pairs_diff_exists':
fixes \<I>::"('a,'b) subst" and D::"('a,'b) dbstate"
assumes "finite D"
shows "\<exists>Di. Di \<subseteq> D \<and> Di \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> {d \<cdot>\<^sub>p \<I>} \<and> d \<cdot>\<^sub>p \<I> \<notin> (D - Di) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
using assms
proof (induction D rule: finite_induct)
case (insert d' D)
then obtain Di where IH: "Di \<subseteq> D" "Di \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> {d \<cdot>\<^sub>p \<I>}" "d \<cdot>\<^sub>p \<I> \<notin> (D - Di) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>" by moura
show ?case
proof (cases "d' \<cdot>\<^sub>p \<I> = d \<cdot>\<^sub>p \<I>")
case True
hence "insert d' Di \<subseteq> insert d' D" "insert d' Di \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> {d \<cdot>\<^sub>p \<I>}"
"d \<cdot>\<^sub>p \<I> \<notin> (insert d' D - insert d' Di) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
using IH by auto
thus ?thesis by metis
next
case False
hence "Di \<subseteq> insert d' D" "Di \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I> \<subseteq> {d \<cdot>\<^sub>p \<I>}"
"d \<cdot>\<^sub>p \<I> \<notin> (insert d' D - Di) \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<I>"
using IH by auto
thus ?thesis by metis
qed
qed simp
lemma stateful_strand_step_subst_inI[intro]:
"send\<langle>t\<rangle> \<in> set A \<Longrightarrow> send\<langle>t \<cdot> \<theta>\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"receive\<langle>t\<rangle> \<in> set A \<Longrightarrow> receive\<langle>t \<cdot> \<theta>\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"\<langle>c: t \<doteq> s\<rangle> \<in> set A \<Longrightarrow> \<langle>c: (t \<cdot> \<theta>) \<doteq> (s \<cdot> \<theta>)\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"insert\<langle>t, s\<rangle> \<in> set A \<Longrightarrow> insert\<langle>t \<cdot> \<theta>, s \<cdot> \<theta>\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"delete\<langle>t, s\<rangle> \<in> set A \<Longrightarrow> delete\<langle>t \<cdot> \<theta>, s \<cdot> \<theta>\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"\<langle>c: t \<in> s\<rangle> \<in> set A \<Longrightarrow> \<langle>c: (t \<cdot> \<theta>) \<in> (s \<cdot> \<theta>)\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle> \<in> set A
\<Longrightarrow> \<forall>X\<langle>\<or>\<noteq>: (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<or>\<notin>: (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>)\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"\<langle>t != s\<rangle> \<in> set A \<Longrightarrow> \<langle>t \<cdot> \<theta> != s \<cdot> \<theta>\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
"\<langle>t not in s\<rangle> \<in> set A \<Longrightarrow> \<langle>t \<cdot> \<theta> not in s \<cdot> \<theta>\<rangle> \<in> set (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
proof (induction A)
case (Cons a A)
note * = subst_sst_cons[of a A \<theta>]
{ case 1 thus ?case using Cons.IH(1) * by (cases a) auto }
{ case 2 thus ?case using Cons.IH(2) * by (cases a) auto }
{ case 3 thus ?case using Cons.IH(3) * by (cases a) auto }
{ case 4 thus ?case using Cons.IH(4) * by (cases a) auto }
{ case 5 thus ?case using Cons.IH(5) * by (cases a) auto }
{ case 6 thus ?case using Cons.IH(6) * by (cases a) auto }
{ case 7 thus ?case using Cons.IH(7) * by (cases a) auto }
{ case 8 thus ?case using Cons.IH(8) * by (cases a) auto }
{ case 9 thus ?case using Cons.IH(9) * by (cases a) auto }
qed simp_all
lemma stateful_strand_step_cases_subst:
"is_Send a = is_Send (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_Receive a = is_Receive (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_Equality a = is_Equality (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_Insert a = is_Insert (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_Delete a = is_Delete (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_InSet a = is_InSet (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_NegChecks a = is_NegChecks (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_Assignment a = is_Assignment (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_Check a = is_Check (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
"is_Update a = is_Update (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
by (cases a; simp_all)+
lemma stateful_strand_step_subst_inv_cases:
"send\<langle>t\<rangle> \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> \<exists>t'. t = t' \<cdot> \<sigma> \<and> send\<langle>t'\<rangle> \<in> set S"
"receive\<langle>t\<rangle> \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> \<exists>t'. t = t' \<cdot> \<sigma> \<and> receive\<langle>t'\<rangle> \<in> set S"
"\<langle>c: t \<doteq> s\<rangle> \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> \<exists>t' s'. t = t' \<cdot> \<sigma> \<and> s = s' \<cdot> \<sigma> \<and> \<langle>c: t' \<doteq> s'\<rangle> \<in> set S"
"insert\<langle>t,s\<rangle> \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> \<exists>t' s'. t = t' \<cdot> \<sigma> \<and> s = s' \<cdot> \<sigma> \<and> insert\<langle>t',s'\<rangle> \<in> set S"
"delete\<langle>t,s\<rangle> \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> \<exists>t' s'. t = t' \<cdot> \<sigma> \<and> s = s' \<cdot> \<sigma> \<and> delete\<langle>t',s'\<rangle> \<in> set S"
"\<langle>c: t \<in> s\<rangle> \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow> \<exists>t' s'. t = t' \<cdot> \<sigma> \<and> s = s' \<cdot> \<sigma> \<and> \<langle>c: t' \<in> s'\<rangle> \<in> set S"
"\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle> \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<Longrightarrow>
\<exists>F' G'. F = F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<sigma> \<and> G = G' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<sigma> \<and>
\<forall>X\<langle>\<or>\<noteq>: F' \<or>\<notin>: G'\<rangle> \<in> set S"
proof (induction S)
case (Cons a S)
have *: "x \<in> set (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>)"
when "x \<in> set (a#S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>)" "x \<noteq> a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<sigma>" for x
using that by (simp add: subst_apply_stateful_strand_def)
{ case 1 thus ?case using Cons.IH(1)[OF *] by (cases a) auto }
{ case 2 thus ?case using Cons.IH(2)[OF *] by (cases a) auto }
{ case 3 thus ?case using Cons.IH(3)[OF *] by (cases a) auto }
{ case 4 thus ?case using Cons.IH(4)[OF *] by (cases a) auto }
{ case 5 thus ?case using Cons.IH(5)[OF *] by (cases a) auto }
{ case 6 thus ?case using Cons.IH(6)[OF *] by (cases a) auto }
{ case 7 thus ?case using Cons.IH(7)[OF *] by (cases a) auto }
qed simp_all
lemma stateful_strand_step_fv_subset_cases:
"send\<langle>t\<rangle> \<in> set S \<Longrightarrow> fv t \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
"receive\<langle>t\<rangle> \<in> set S \<Longrightarrow> fv t \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
"\<langle>c: t \<doteq> s\<rangle> \<in> set S \<Longrightarrow> fv t \<union> fv s \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
"insert\<langle>t,s\<rangle> \<in> set S \<Longrightarrow> fv t \<union> fv s \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
"delete\<langle>t,s\<rangle> \<in> set S \<Longrightarrow> fv t \<union> fv s \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
"\<langle>c: t \<in> s\<rangle> \<in> set S \<Longrightarrow> fv t \<union> fv s \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
"\<forall>X\<langle>\<or>\<noteq>: F \<or>\<notin>: G\<rangle> \<in> set S \<Longrightarrow> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G - set X \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t S"
proof (induction S)
case (Cons a S)
{ case 1 thus ?case using Cons.IH(1) by auto }
{ case 2 thus ?case using Cons.IH(2) by auto }
{ case 3 thus ?case using Cons.IH(3) by auto }
{ case 4 thus ?case using Cons.IH(4) by auto }
{ case 5 thus ?case using Cons.IH(5) by auto }
{ case 6 thus ?case using Cons.IH(6) by auto }
{ case 7 thus ?case using Cons.IH(7) by fastforce }
qed simp_all
lemma trms\<^sub>s\<^sub>s\<^sub>t_nil[simp]:
"trms\<^sub>s\<^sub>s\<^sub>t [] = {}"
unfolding trms\<^sub>s\<^sub>s\<^sub>t_def by simp
lemma trms\<^sub>s\<^sub>s\<^sub>t_mono:
"set M \<subseteq> set N \<Longrightarrow> trms\<^sub>s\<^sub>s\<^sub>t M \<subseteq> trms\<^sub>s\<^sub>s\<^sub>t N"
by auto
lemma trms\<^sub>s\<^sub>s\<^sub>t_in:
assumes "t \<in> trms\<^sub>s\<^sub>s\<^sub>t S"
shows "\<exists>a \<in> set S. t \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a"
using assms unfolding trms\<^sub>s\<^sub>s\<^sub>t_def by simp
lemma trms\<^sub>s\<^sub>s\<^sub>t_cons: "trms\<^sub>s\<^sub>s\<^sub>t (a#A) = trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<union> trms\<^sub>s\<^sub>s\<^sub>t A"
unfolding trms\<^sub>s\<^sub>s\<^sub>t_def by force
lemma trms\<^sub>s\<^sub>s\<^sub>t_append[simp]: "trms\<^sub>s\<^sub>s\<^sub>t (A@B) = trms\<^sub>s\<^sub>s\<^sub>t A \<union> trms\<^sub>s\<^sub>s\<^sub>t B"
unfolding trms\<^sub>s\<^sub>s\<^sub>t_def by force
lemma trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst:
assumes "set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a) \<inter> subst_domain \<theta> = {}"
shows "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
proof (cases a)
case (NegChecks X F G)
hence "rm_vars (set X) \<theta> = \<theta>" using assms rm_vars_apply'[of \<theta> "set X"] by auto
hence "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>) \<union> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>)"
"trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta> = (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>) \<union> (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>)"
using NegChecks image_Un by simp_all
thus ?thesis by (metis trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst)
qed simp_all
lemma trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst':
assumes "\<not>is_NegChecks a"
shows "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
using assms by (cases a) simp_all
lemma trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst'':
fixes t::"('a,'b) term" and \<delta>::"('a,'b) subst"
assumes "t \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (b \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
shows "\<exists>s \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p b. t = s \<cdot> rm_vars (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p b)) \<delta>"
proof (cases "is_NegChecks b")
case True
then obtain X F G where *: "b = NegChecks X F G" by (cases b) moura+
thus ?thesis using assms trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst[of _ "rm_vars (set X) \<delta>"] by auto
next
case False
hence "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (b \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) = trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p b \<cdot>\<^sub>s\<^sub>e\<^sub>t rm_vars (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p b)) \<delta>"
using trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst' bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegChecks
by fastforce
thus ?thesis using assms by fast
qed
lemma trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst''':
fixes t::"('a,'b) term" and \<delta> \<theta>::"('a,'b) subst"
assumes "t \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (b \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
shows "\<exists>s \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p b. t = s \<cdot> rm_vars (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p b)) \<delta> \<circ>\<^sub>s \<theta>"
proof -
obtain s where s: "s \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (b \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)" "t = s \<cdot> \<theta>" using assms by moura
show ?thesis using trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst''[OF s(1)] s(2) by auto
qed
lemma trms\<^sub>s\<^sub>s\<^sub>t_subst:
assumes "bvars\<^sub>s\<^sub>s\<^sub>t S \<inter> subst_domain \<theta> = {}"
shows "trms\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>) = trms\<^sub>s\<^sub>s\<^sub>t S \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
using assms
proof (induction S)
case (Cons a S)
hence IH: "trms\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>) = trms\<^sub>s\<^sub>s\<^sub>t S \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>" and *: "set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a) \<inter> subst_domain \<theta> = {}"
by auto
show ?case using trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst[OF *] IH by (auto simp add: subst_apply_stateful_strand_def)
qed simp
lemma trms\<^sub>s\<^sub>s\<^sub>t_subst_cons:
"trms\<^sub>s\<^sub>s\<^sub>t (a#A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>) = trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) \<union> trms\<^sub>s\<^sub>s\<^sub>t (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
using subst_sst_cons[of a A \<delta>] trms\<^sub>s\<^sub>s\<^sub>t_cons[of a A] trms\<^sub>s\<^sub>s\<^sub>t_append by simp
lemma (in intruder_model) wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst:
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)"
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>))"
using assms
proof (cases a)
case (NegChecks X F G)
hence *: "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) =
(trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>)) \<union> (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>))"
by simp
have "trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> = (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>) \<union> (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)"
using NegChecks image_Un by simp
hence "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)" using * assms by auto
hence "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<cdot>\<^sub>s\<^sub>e\<^sub>t rm_vars (set X) \<delta>)"
"wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G \<cdot>\<^sub>s\<^sub>e\<^sub>t rm_vars (set X) \<delta>)"
using wf_trms_subst_rm_vars[of \<delta> "trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F" "set X"]
wf_trms_subst_rm_vars[of \<delta> "trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" "set X"]
by fast+
thus ?thesis
using * trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst[of _ "rm_vars (set X) \<delta>"]
by auto
qed auto
lemma trms\<^sub>s\<^sub>s\<^sub>t_fv_vars\<^sub>s\<^sub>s\<^sub>t_subset: "t \<in> trms\<^sub>s\<^sub>s\<^sub>t A \<Longrightarrow> fv t \<subseteq> vars\<^sub>s\<^sub>s\<^sub>t A"
proof (induction A)
case (Cons a A) thus ?case by (cases a) auto
qed simp
lemma trms\<^sub>s\<^sub>s\<^sub>t_fv_subst_subset:
assumes "t \<in> trms\<^sub>s\<^sub>s\<^sub>t S" "subst_domain \<theta> \<inter> bvars\<^sub>s\<^sub>s\<^sub>t S = {}"
shows "fv (t \<cdot> \<theta>) \<subseteq> vars\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
using assms
proof (induction S)
case (Cons s S) show ?case
proof (cases "t \<in> trms\<^sub>s\<^sub>s\<^sub>t S")
case True
hence "fv (t \<cdot> \<theta>) \<subseteq> vars\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)" using Cons.IH Cons.prems by auto
thus ?thesis using subst_sst_cons[of s S \<theta>] unfolding vars\<^sub>s\<^sub>s\<^sub>t_def by auto
next
case False
hence *: "t \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p s" "subst_domain \<theta> \<inter> set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s) = {}" using Cons.prems by auto
hence "fv (t \<cdot> \<theta>) \<subseteq> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
proof (cases s)
case (NegChecks X F G)
hence **: "t \<in> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<or> t \<in> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" using *(1) by auto
have ***: "rm_vars (set X) \<theta> = \<theta>" using *(2) NegChecks rm_vars_apply' by auto
have "fv (t \<cdot> \<theta>) \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>)"
using ** *** trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_fv_subst_subset[of t _ \<theta>] by auto
thus ?thesis using *(2) using NegChecks vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(7)[of X F G \<theta>] by blast
qed auto
thus ?thesis using subst_sst_cons[of s S \<theta>] unfolding vars\<^sub>s\<^sub>s\<^sub>t_def by auto
qed
qed simp
lemma trms\<^sub>s\<^sub>s\<^sub>t_fv_subst_subset':
assumes "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S)" "fv t \<inter> bvars\<^sub>s\<^sub>s\<^sub>t S = {}" "fv (t \<cdot> \<theta>) \<inter> bvars\<^sub>s\<^sub>s\<^sub>t S = {}"
shows "fv (t \<cdot> \<theta>) \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
using assms
proof (induction S)
case (Cons s S) show ?case
proof (cases "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S)")
case True
hence "fv (t \<cdot> \<theta>) \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)" using Cons.IH Cons.prems by auto
thus ?thesis using subst_sst_cons[of s S \<theta>] unfolding vars\<^sub>s\<^sub>s\<^sub>t_def by auto
next
case False
hence 0: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p s)" "fv t \<inter> set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s) = {}"
"fv (t \<cdot> \<theta>) \<inter> set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s) = {}"
using Cons.prems by auto
note 1 = UN_Un UN_insert fv\<^sub>s\<^sub>e\<^sub>t.simps subst_apply_fv_subset subst_apply_fv_unfold
subst_apply_term_empty sup_bot.comm_neutral fv_subterms_set fv_subset[OF 0(1)]
note 2 = subst_apply_fv_union
have "fv (t \<cdot> \<theta>) \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
proof (cases s)
case (NegChecks X F G)
hence 3: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<or> t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G)" using 0(1) by auto
have "t \<cdot> rm_vars (set X) \<theta> = t \<cdot> \<theta>" using 0(2) NegChecks rm_vars_ident[of t] by auto
hence "fv (t \<cdot> \<theta>) \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>)"
using 3 trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_fv_subst_subset'[of t _ "rm_vars (set X) \<theta>"] by fastforce
thus ?thesis using 0(2,3) NegChecks fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(7)[of X F G \<theta>] by auto
qed (metis (no_types, lifting) 1 trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p.simps(1) fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(1),
metis (no_types, lifting) 1 trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p.simps(2) fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(2),
metis (no_types, lifting) 1 2 trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p.simps(3) fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(3),
metis (no_types, lifting) 1 2 trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p.simps(4) fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(4),
metis (no_types, lifting) 1 2 trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p.simps(5) fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(5),
metis (no_types, lifting) 1 2 trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p.simps(6) fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases(6))
thus ?thesis using subst_sst_cons[of s S \<theta>] unfolding fv\<^sub>s\<^sub>s\<^sub>t_def by auto
qed
qed simp
lemma trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_funs_term_cases:
assumes "t \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)" "f \<in> funs_term t"
shows "(\<exists>u \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p s. f \<in> funs_term u) \<or> (\<exists>x \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p s. f \<in> funs_term (\<theta> x))"
using assms
proof (cases s)
case (NegChecks X F G)
hence "t \<in> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>) \<or> t \<in> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>)"
using assms(1) by auto
hence "(\<exists>u\<in>trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F. f \<in> funs_term u) \<or> (\<exists>x\<in>fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F. f \<in> funs_term (rm_vars (set X) \<theta> x)) \<or>
(\<exists>u\<in>trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G. f \<in> funs_term u) \<or> (\<exists>x\<in>fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G. f \<in> funs_term (rm_vars (set X) \<theta> x))"
using trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_funs_term_cases[OF _ assms(2), of _ "rm_vars (set X) \<theta>"] by meson
hence "(\<exists>u \<in> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G. f \<in> funs_term u) \<or>
(\<exists>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G. f \<in> funs_term (rm_vars (set X) \<theta> x))"
by blast
thus ?thesis
proof
assume "\<exists>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G. f \<in> funs_term (rm_vars (set X) \<theta> x)"
then obtain x where x: "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" "f \<in> funs_term (rm_vars (set X) \<theta> x)"
by auto
hence "x \<notin> set X" "rm_vars (set X) \<theta> x = \<theta> x" by auto
thus ?thesis using x by (auto simp add: assms NegChecks)
qed (auto simp add: assms NegChecks)
qed (use assms funs_term_subst[of _ \<theta>] in auto)
lemma trms\<^sub>s\<^sub>s\<^sub>t_funs_term_cases:
assumes "t \<in> trms\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)" "f \<in> funs_term t"
shows "(\<exists>u \<in> trms\<^sub>s\<^sub>s\<^sub>t S. f \<in> funs_term u) \<or> (\<exists>x \<in> fv\<^sub>s\<^sub>s\<^sub>t S. f \<in> funs_term (\<theta> x))"
using assms(1)
proof (induction S)
case (Cons s S) thus ?case
proof (cases "t \<in> trms\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)")
case False
hence "t \<in> trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)" using Cons.prems(1) subst_sst_cons[of s S \<theta>] trms\<^sub>s\<^sub>s\<^sub>t_cons by auto
thus ?thesis using trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_funs_term_cases[OF _ assms(2)] by fastforce
qed auto
qed simp
lemma fv\<^sub>s\<^sub>s\<^sub>t_is_subterm_trms\<^sub>s\<^sub>s\<^sub>t_subst:
assumes "x \<in> fv\<^sub>s\<^sub>s\<^sub>t T"
and "bvars\<^sub>s\<^sub>s\<^sub>t T \<inter> subst_domain \<theta> = {}"
shows "\<theta> x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t (T \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>))"
using trms\<^sub>s\<^sub>s\<^sub>t_subst[OF assms(2)] subterms_subst_subset'[of \<theta> "trms\<^sub>s\<^sub>s\<^sub>t T"]
fv\<^sub>s\<^sub>s\<^sub>t_is_subterm_trms\<^sub>s\<^sub>s\<^sub>t[OF assms(1)]
by (metis (no_types, lifting) image_iff subset_iff subst_apply_term.simps(1))
lemma fv\<^sub>s\<^sub>s\<^sub>t_subst_fv_subset:
assumes "x \<in> fv\<^sub>s\<^sub>s\<^sub>t S" "x \<notin> bvars\<^sub>s\<^sub>s\<^sub>t S" "fv (\<theta> x) \<inter> bvars\<^sub>s\<^sub>s\<^sub>t S = {}"
shows "fv (\<theta> x) \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>)"
using assms
proof (induction S)
case (Cons a S)
note 1 = fv_subst_subset[of _ _ \<theta>]
note 2 = subst_apply_fv_union subst_apply_fv_unfold[of _ \<theta>] fv_subset image_eqI
note 3 = fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst_cases
note 4 = fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p.simps
from Cons show ?case
proof (cases "x \<in> fv\<^sub>s\<^sub>s\<^sub>t S")
case False
hence 5: "x \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p a" " fv (\<theta> x) \<inter> set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a) = {}" "x \<notin> set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a)"
using Cons.prems by auto
hence "fv (\<theta> x) \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>)"
proof (cases a)
case (NegChecks X F G)
let ?\<delta> = "rm_vars (set X) \<theta>"
have *: "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" using NegChecks 5(1) by auto
have **: "fv (\<theta> x) \<inter> set X = {}" using NegChecks 5(2) by simp
have ***: "\<theta> x = ?\<delta> x" using NegChecks 5(3) by auto
have "fv (\<theta> x) \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<delta>) \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<delta>)"
using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst_fv_subset[of x _ ?\<delta>] * *** by auto
thus ?thesis using NegChecks ** by auto
qed (metis (full_types) 1 5(1) 3(1) 4(1), metis (full_types) 1 5(1) 3(2) 4(2),
metis (full_types) 2 5(1) 3(3) 4(3), metis (full_types) 2 5(1) 3(4) 4(4),
metis (full_types) 2 5(1) 3(5) 4(5), metis (full_types) 2 5(1) 3(6) 4(6))
thus ?thesis by (auto simp add: subst_sst_cons[of a S \<theta>])
qed (auto simp add: subst_sst_cons[of a S \<theta>])
qed simp
lemma (in intruder_model) wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_trms\<^sub>s\<^sub>s\<^sub>t_subst:
assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)"
shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>))"
using assms
proof (induction A)
case (Cons a A)
hence IH: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t (A \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>))" and *: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)" by auto
have "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>))" by (rule wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst[OF *])
thus ?case using IH trms\<^sub>s\<^sub>s\<^sub>t_subst_cons[of a A \<delta>] by blast
qed simp
lemma fv\<^sub>s\<^sub>s\<^sub>t_subst_obtain_var:
assumes "x \<in> fv\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
shows "\<exists>y \<in> fv\<^sub>s\<^sub>s\<^sub>t S. x \<in> fv (\<delta> y)"
using assms
proof (induction S)
case (Cons s S)
hence "x \<in> fv\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>) \<Longrightarrow> \<exists>y \<in> fv\<^sub>s\<^sub>s\<^sub>t S. x \<in> fv (\<delta> y)"
using bvars\<^sub>s\<^sub>s\<^sub>t_cons_subset[of S s]
by blast
thus ?case
proof (cases "x \<in> fv\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)")
case False
hence *: "x \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
using Cons.prems(1) subst_sst_cons[of s S \<delta>]
by fastforce
have "\<exists>y \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p s. x \<in> fv (\<delta> y)"
proof (cases s)
case (NegChecks X F G)
hence "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>) \<or> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>)"
and **: "x \<notin> set X"
using * by simp_all
then obtain y where y: "y \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<or> y \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" "x \<in> fv ((rm_vars (set X) \<delta>) y)"
using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst_obtain_var[of _ _ "rm_vars (set X) \<delta>"]
by blast
have "y \<notin> set X"
proof
assume y_in: "y \<in> set X"
hence "(rm_vars (set X) \<delta>) y = Var y" by auto
hence "x = y" using y(2) by simp
thus False using ** y_in by metis
qed
thus ?thesis using NegChecks y by auto
qed (use * fv_subst_obtain_var in force)+
thus ?thesis by auto
qed auto
qed simp
lemma fv\<^sub>s\<^sub>s\<^sub>t_subst_subset_range_vars_if_subset_domain:
assumes "fv\<^sub>s\<^sub>s\<^sub>t S \<subseteq> subst_domain \<sigma>"
shows "fv\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<sigma>) \<subseteq> range_vars \<sigma>"
using assms fv\<^sub>s\<^sub>s\<^sub>t_subst_obtain_var[of _ S \<sigma>] subst_dom_vars_in_subst[of _ \<sigma>] subst_fv_imgI[of \<sigma>]
by (metis (no_types) in_mono subsetI)
lemma fv\<^sub>s\<^sub>s\<^sub>t_in_fv_trms\<^sub>s\<^sub>s\<^sub>t: "x \<in> fv\<^sub>s\<^sub>s\<^sub>t S \<Longrightarrow> x \<in> fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t S)"
proof (induction S)
case (Cons s S) thus ?case
proof (cases "x \<in> fv\<^sub>s\<^sub>s\<^sub>t S")
case False
hence *: "x \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p s" using Cons.prems by simp
hence "x \<in> fv\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>s\<^sub>t\<^sub>p s)"
proof (cases s)
case (NegChecks X F G)
hence "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<or> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" using * by simp_all
thus ?thesis using * fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_in_fv_trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s[of x] NegChecks by auto
qed auto
thus ?thesis by simp
qed simp
qed simp
lemma stateful_strand_step_subst_comp:
assumes "range_vars \<delta> \<inter> set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p x) = {}"
shows "x \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta> \<circ>\<^sub>s \<theta> = (x \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>"
proof (cases x)
case (NegChecks X F G)
hence *: "range_vars \<delta> \<inter> set X = {}" using assms by simp
have "H \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) (\<delta> \<circ>\<^sub>s \<theta>) = (H \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>) \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<theta>" for H
using pairs_subst_comp rm_vars_comp[OF *] by (induct H) (auto simp add: subst_apply_pairs_def)
thus ?thesis using NegChecks by simp
qed simp_all
lemma stateful_strand_subst_comp:
assumes "range_vars \<delta> \<inter> bvars\<^sub>s\<^sub>s\<^sub>t S = {}"
shows "S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta> \<circ>\<^sub>s \<theta> = (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>"
using assms
proof (induction S)
case (Cons s S)
hence IH: "S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta> \<circ>\<^sub>s \<theta> = (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>" using Cons by auto
have "s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta> \<circ>\<^sub>s \<theta> = (s \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>"
using Cons.prems stateful_strand_step_subst_comp[of \<delta> s \<theta>]
unfolding range_vars_alt_def by auto
thus ?case using IH by (simp add: subst_apply_stateful_strand_def)
qed simp
lemma subst_apply_bvars_disj_NegChecks:
assumes "set X \<inter> subst_domain \<theta> = {}"
shows "NegChecks X F G \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = NegChecks X (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>) (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>)"
proof -
have "rm_vars (set X) \<theta> = \<theta>" using assms rm_vars_apply'[of \<theta> "set X"] by auto
thus ?thesis by simp
qed
lemma subst_apply_NegChecks_no_bvars[simp]:
"\<forall>[]\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<forall>[]\<langle>\<or>\<noteq>: (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>) \<or>\<notin>: (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>)\<rangle>"
"\<forall>[]\<langle>\<or>\<noteq>: [] \<or>\<notin>: F'\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<forall>[]\<langle>\<or>\<noteq>: [] \<or>\<notin>: (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>)\<rangle>"
"\<forall>[]\<langle>\<or>\<noteq>: F \<or>\<notin>: []\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<forall>[]\<langle>\<or>\<noteq>: (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>) \<or>\<notin>: []\<rangle>"
"\<forall>[]\<langle>\<or>\<noteq>: [] \<or>\<notin>: [(t,s)]\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<forall>[]\<langle>\<or>\<noteq>: [] \<or>\<notin>: ([(t \<cdot> \<theta>,s \<cdot> \<theta>)])\<rangle>" (is ?A)
"\<forall>[]\<langle>\<or>\<noteq>: [(t,s)] \<or>\<notin>: []\<rangle> \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta> = \<forall>[]\<langle>\<or>\<noteq>: ([(t \<cdot> \<theta>,s \<cdot> \<theta>)]) \<or>\<notin>: []\<rangle>" (is ?B)
by simp_all
lemma setops\<^sub>s\<^sub>s\<^sub>t_mono:
"set M \<subseteq> set N \<Longrightarrow> setops\<^sub>s\<^sub>s\<^sub>t M \<subseteq> setops\<^sub>s\<^sub>s\<^sub>t N"
by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
lemma setops\<^sub>s\<^sub>s\<^sub>t_nil[simp]: "setops\<^sub>s\<^sub>s\<^sub>t [] = {}"
by (simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
lemma setops\<^sub>s\<^sub>s\<^sub>t_cons[simp]: "setops\<^sub>s\<^sub>s\<^sub>t (a#A) = setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<union> setops\<^sub>s\<^sub>s\<^sub>t A"
by (simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
lemma setops\<^sub>s\<^sub>s\<^sub>t_cons_subset[simp]: "setops\<^sub>s\<^sub>s\<^sub>t A \<subseteq> setops\<^sub>s\<^sub>s\<^sub>t (a#A)"
using setops\<^sub>s\<^sub>s\<^sub>t_cons[of a A] by blast
lemma setops\<^sub>s\<^sub>s\<^sub>t_append: "setops\<^sub>s\<^sub>s\<^sub>t (A@B) = setops\<^sub>s\<^sub>s\<^sub>t A \<union> setops\<^sub>s\<^sub>s\<^sub>t B"
proof (induction A)
case (Cons a A) thus ?case by (cases a) (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
qed (simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
lemma setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_member_iff:
"(t,s) \<in> setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p x \<longleftrightarrow>
(x = Insert t s \<or> x = Delete t s \<or> (\<exists>ac. x = InSet ac t s) \<or>
(\<exists>X F F'. x = NegChecks X F F' \<and> (t,s) \<in> set F'))"
by (cases x) auto
lemma setops\<^sub>s\<^sub>s\<^sub>t_member_iff:
"(t,s) \<in> setops\<^sub>s\<^sub>s\<^sub>t A \<longleftrightarrow>
(Insert t s \<in> set A \<or> Delete t s \<in> set A \<or> (\<exists>ac. InSet ac t s \<in> set A) \<or>
(\<exists>X F F'. NegChecks X F F' \<in> set A \<and> (t,s) \<in> set F'))"
(is "?P \<longleftrightarrow> ?Q")
proof (induction A)
case (Cons a A) thus ?case
proof (cases "(t, s) \<in> setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p a")
case True thus ?thesis using setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_member_iff[of t s a] by auto
qed auto
qed simp
lemma setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst:
assumes "set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a) \<inter> subst_domain \<theta> = {}"
shows "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<theta>"
proof (cases a)
case (NegChecks X F G)
hence "rm_vars (set X) \<theta> = \<theta>" using assms rm_vars_apply'[of \<theta> "set X"] by auto
hence "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = set (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<theta>)"
"setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<theta> = set G \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<theta>"
using NegChecks image_Un by simp_all
thus ?thesis by (simp add: subst_apply_pairs_def)
qed simp_all
lemma setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst':
assumes "\<not>is_NegChecks a"
shows "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<theta>) = setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p a \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<theta>"
using assms by (cases a) auto
lemma setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst'':
fixes t::"('a,'b) term \<times> ('a,'b) term" and \<delta>::"('a,'b) subst"
assumes t: "t \<in> setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (b \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
shows "\<exists>s \<in> setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p b. t = s \<cdot>\<^sub>p rm_vars (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p b)) \<delta>"
proof (cases "is_NegChecks b")
case True
then obtain X F G where b: "b = NegChecks X F G" by (cases b) moura+
hence "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p b = set G" "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (b \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) = set (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p b)) \<delta>)"
by simp_all
thus ?thesis using t subst_apply_pairs_pset_subst[of G] by blast
next
case False
hence "setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (b \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>) = setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p b \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t rm_vars (set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p b)) \<delta>"
using setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst' bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegChecks by fastforce
thus ?thesis using t by blast
qed
lemma setops\<^sub>s\<^sub>s\<^sub>t_subst:
assumes "bvars\<^sub>s\<^sub>s\<^sub>t S \<inter> subst_domain \<theta> = {}"
shows "setops\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>) = setops\<^sub>s\<^sub>s\<^sub>t S \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<theta>"
using assms
proof (induction S)
case (Cons a S)
have "bvars\<^sub>s\<^sub>s\<^sub>t S \<inter> subst_domain \<theta> = {}" and *: "set (bvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a) \<inter> subst_domain \<theta> = {}"
using Cons.prems by auto
hence IH: "setops\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<theta>) = setops\<^sub>s\<^sub>s\<^sub>t S \<cdot>\<^sub>p\<^sub>s\<^sub>e\<^sub>t \<theta>"
using Cons.IH by auto
show ?case
using setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst[OF *] IH unfolding setops\<^sub>s\<^sub>s\<^sub>t_def
by (auto simp add: subst_apply_stateful_strand_def)
qed (simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
lemma setops\<^sub>s\<^sub>s\<^sub>t_subst':
fixes p::"('a,'b) term \<times> ('a,'b) term" and \<delta>::"('a,'b) subst"
assumes "p \<in> setops\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
shows "\<exists>s \<in> setops\<^sub>s\<^sub>s\<^sub>t S. \<exists>X. set X \<subseteq> bvars\<^sub>s\<^sub>s\<^sub>t S \<and> p = s \<cdot>\<^sub>p rm_vars (set X) \<delta>"
using assms
proof (induction S)
case (Cons a S)
note 0 = setops\<^sub>s\<^sub>s\<^sub>t_cons[of a S] bvars\<^sub>s\<^sub>s\<^sub>t_Cons[of a S]
note 1 = setops\<^sub>s\<^sub>s\<^sub>t_cons[of "a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>" "S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>"] subst_sst_cons[of a S \<delta>]
have "p \<in> setops\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>) \<or> p \<in> setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)" using Cons.prems 1 by auto
thus ?case
proof
assume *: "p \<in> setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
show ?thesis using setops\<^sub>s\<^sub>s\<^sub>t\<^sub>p_subst''[OF *] 0 by blast
next
assume *: "p \<in> setops\<^sub>s\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
show ?thesis using Cons.IH[OF *] 0 by blast
qed
qed simp
subsection \<open>Stateful Constraint Semantics\<close>
context intruder_model
begin
definition negchecks_model where
"negchecks_model (\<I>::('a,'b) subst) (D::('a,'b) dbstate) X F G \<equiv>
(\<forall>\<delta>. subst_domain \<delta> = set X \<and> ground (subst_range \<delta>) \<longrightarrow>
(list_ex (\<lambda>f. fst f \<cdot> (\<delta> \<circ>\<^sub>s \<I>) \<noteq> snd f \<cdot> (\<delta> \<circ>\<^sub>s \<I>)) F \<or>
list_ex (\<lambda>f. f \<cdot>\<^sub>p (\<delta> \<circ>\<^sub>s \<I>) \<notin> D) G))"
fun strand_sem_stateful::
"('fun,'var) terms \<Rightarrow> ('fun,'var) dbstate \<Rightarrow> ('fun,'var) stateful_strand \<Rightarrow> ('fun,'var) subst \<Rightarrow> bool"
("\<lbrakk>_; _; _\<rbrakk>\<^sub>s")
where
"\<lbrakk>M; D; []\<rbrakk>\<^sub>s = (\<lambda>\<I>. True)"
| "\<lbrakk>M; D; Send t#S\<rbrakk>\<^sub>s = (\<lambda>\<I>. M \<turnstile> t \<cdot> \<I> \<and> \<lbrakk>M; D; S\<rbrakk>\<^sub>s \<I>)"
| "\<lbrakk>M; D; Receive t#S\<rbrakk>\<^sub>s = (\<lambda>\<I>. \<lbrakk>insert (t \<cdot> \<I>) M; D; S\<rbrakk>\<^sub>s \<I>)"
| "\<lbrakk>M; D; Equality _ t t'#S\<rbrakk>\<^sub>s = (\<lambda>\<I>. t \<cdot> \<I> = t' \<cdot> \<I> \<and> \<lbrakk>M; D; S\<rbrakk>\<^sub>s \<I>)"
| "\<lbrakk>M; D; Insert t s#S\<rbrakk>\<^sub>s = (\<lambda>\<I>. \<lbrakk>M; insert ((t,s) \<cdot>\<^sub>p \<I>) D; S\<rbrakk>\<^sub>s \<I>)"
| "\<lbrakk>M; D; Delete t s#S\<rbrakk>\<^sub>s = (\<lambda>\<I>. \<lbrakk>M; D - {(t,s) \<cdot>\<^sub>p \<I>}; S\<rbrakk>\<^sub>s \<I>)"
| "\<lbrakk>M; D; InSet _ t s#S\<rbrakk>\<^sub>s = (\<lambda>\<I>. (t,s) \<cdot>\<^sub>p \<I> \<in> D \<and> \<lbrakk>M; D; S\<rbrakk>\<^sub>s \<I>)"
| "\<lbrakk>M; D; NegChecks X F F'#S\<rbrakk>\<^sub>s = (\<lambda>\<I>. negchecks_model \<I> D X F F' \<and> \<lbrakk>M; D; S\<rbrakk>\<^sub>s \<I>)"
lemmas strand_sem_stateful_induct =
strand_sem_stateful.induct[case_names Nil ConsSnd ConsRcv ConsEq
ConsIns ConsDel ConsIn ConsNegChecks]
abbreviation constr_sem_stateful (infix "\<Turnstile>\<^sub>s" 91) where "\<I> \<Turnstile>\<^sub>s A \<equiv> \<lbrakk>{}; {}; A\<rbrakk>\<^sub>s \<I>"
lemma stateful_strand_sem_NegChecks_no_bvars:
"\<lbrakk>M; D; [\<langle>t not in s\<rangle>]\<rbrakk>\<^sub>s \<I> \<Longrightarrow> (t \<cdot> \<I>, s \<cdot> \<I>) \<notin> D"
"\<lbrakk>M; D; [\<langle>t != s\<rangle>]\<rbrakk>\<^sub>s \<I> \<Longrightarrow> t \<cdot> \<I> \<noteq> s \<cdot> \<I>"
by (simp_all add: negchecks_model_def empty_dom_iff_empty_subst)
lemma strand_sem_ik_mono_stateful:
"\<lbrakk>M; D; A\<rbrakk>\<^sub>s \<I> \<Longrightarrow> \<lbrakk>M \<union> M'; D; A\<rbrakk>\<^sub>s \<I>"
using ideduct_mono by (induct A arbitrary: M M' D rule: strand_sem_stateful.induct) force+
lemma strand_sem_append_stateful:
"\<lbrakk>M; D; A@B\<rbrakk>\<^sub>s \<I> \<longleftrightarrow> \<lbrakk>M; D; A\<rbrakk>\<^sub>s \<I> \<and> \<lbrakk>M \<union> (ik\<^sub>s\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>); dbupd\<^sub>s\<^sub>s\<^sub>t A \<I> D; B\<rbrakk>\<^sub>s \<I>"
(is "?P \<longleftrightarrow> ?Q \<and> ?R")
proof -
have 1: "?P \<Longrightarrow> ?Q" by (induct A rule: strand_sem_stateful.induct) auto
have 2: "?P \<Longrightarrow> ?R"
proof (induction A arbitrary: M D B)
case (Cons a A) thus ?case
proof (cases a)
case (Receive t)
have "insert (t \<cdot> \<I>) (M \<union> (ik\<^sub>s\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)) = M \<union> (ik\<^sub>s\<^sub>s\<^sub>t (a#A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)"
"dbupd\<^sub>s\<^sub>s\<^sub>t A \<I> D = dbupd\<^sub>s\<^sub>s\<^sub>t (a#A) \<I> D"
using Receive by (auto simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
thus ?thesis using Cons Receive by force
qed (auto simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
qed (simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
have 3: "?Q \<Longrightarrow> ?R \<Longrightarrow> ?P"
proof (induction A arbitrary: M D)
case (Cons a A) thus ?case
proof (cases a)
case (Receive t)
have "insert (t \<cdot> \<I>) (M \<union> (ik\<^sub>s\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)) = M \<union> (ik\<^sub>s\<^sub>s\<^sub>t (a#A) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)"
"dbupd\<^sub>s\<^sub>s\<^sub>t A \<I> D = dbupd\<^sub>s\<^sub>s\<^sub>t (a#A) \<I> D"
using Receive by (auto simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
thus ?thesis using Cons Receive by simp
qed (auto simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
qed (simp add: ik\<^sub>s\<^sub>s\<^sub>t_def)
show ?thesis by (metis 1 2 3)
qed
lemma negchecks_model_db_subset:
fixes F F'::"(('a,'b) term \<times> ('a,'b) term) list"
assumes "D' \<subseteq> D"
and "negchecks_model \<I> D X F F'"
shows "negchecks_model \<I> D' X F F'"
proof -
have "list_ex (\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D') F'"
when "list_ex (\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D) F'"
for \<delta>::"('a,'b) subst"
using Bex_set[of F' "\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D'"]
Bex_set[of F' "\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D"]
that assms(1)
by blast
thus ?thesis using assms(2) by (auto simp add: negchecks_model_def)
qed
lemma negchecks_model_db_supset:
fixes F F'::"(('a,'b) term \<times> ('a,'b) term) list"
assumes "D' \<subseteq> D"
and "\<forall>f \<in> set F'. \<forall>\<delta>. subst_domain \<delta> = set X \<and> ground (subst_range \<delta>) \<longrightarrow> f \<cdot>\<^sub>p (\<delta> \<circ>\<^sub>s \<I>) \<notin> D - D'"
and "negchecks_model \<I> D' X F F'"
shows "negchecks_model \<I> D X F F'"
proof -
have "list_ex (\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D) F'"
when "list_ex (\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D') F'" "subst_domain \<delta> = set X \<and> ground (subst_range \<delta>)"
for \<delta>::"('a,'b) subst"
using Bex_set[of F' "\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D'"]
Bex_set[of F' "\<lambda>f. f \<cdot>\<^sub>p \<delta> \<circ>\<^sub>s \<I> \<notin> D"]
that assms(1,2)
by blast
thus ?thesis using assms(3) by (auto simp add: negchecks_model_def)
qed
lemma negchecks_model_subst:
fixes F F'::"(('a,'b) term \<times> ('a,'b) term) list"
assumes "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> set X = {}"
shows "negchecks_model (\<delta> \<circ>\<^sub>s \<theta>) D X F F' \<longleftrightarrow> negchecks_model \<theta> D X (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>) (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
proof -
have 0: "\<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) = \<delta> \<circ>\<^sub>s (\<sigma> \<circ>\<^sub>s \<theta>)"
when \<sigma>: "subst_domain \<sigma> = set X" "ground (subst_range \<sigma>)" for \<sigma>
by (metis (no_types, lifting) \<sigma> subst_compose_assoc assms(1) inf_sup_aci(1)
subst_comp_eq_if_disjoint_vars sup_inf_absorb range_vars_alt_def)
{ fix \<sigma>::"('a,'b) subst" and t t'
assume \<sigma>: "subst_domain \<sigma> = set X" "ground (subst_range \<sigma>)"
and *: "list_ex (\<lambda>f. fst f \<cdot> (\<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>)) \<noteq> snd f \<cdot> (\<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>))) F"
obtain f where f: "f \<in> set F" "fst f \<cdot> \<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) \<noteq> snd f \<cdot> \<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>)"
using * by (induct F) auto
hence "(fst f \<cdot> \<delta>) \<cdot> \<sigma> \<circ>\<^sub>s \<theta> \<noteq> (snd f \<cdot> \<delta>) \<cdot> \<sigma> \<circ>\<^sub>s \<theta>" using 0[OF \<sigma>] by simp
moreover have "(fst f \<cdot> \<delta>, snd f \<cdot> \<delta>) \<in> set (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
using f(1) by (auto simp add: subst_apply_pairs_def)
ultimately have "list_ex (\<lambda>f. fst f \<cdot> (\<sigma> \<circ>\<^sub>s \<theta>) \<noteq> snd f \<cdot> (\<sigma> \<circ>\<^sub>s \<theta>)) (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
using f(1) Bex_set by fastforce
} moreover {
fix \<sigma>::"('a,'b) subst" and t t'
assume \<sigma>: "subst_domain \<sigma> = set X" "ground (subst_range \<sigma>)"
and *: "list_ex (\<lambda>f. f \<cdot>\<^sub>p \<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) \<notin> D) F'"
obtain f where f: "f \<in> set F'" "f \<cdot>\<^sub>p \<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) \<notin> D"
using * by (induct F') auto
hence "f \<cdot>\<^sub>p \<delta> \<cdot>\<^sub>p \<sigma> \<circ>\<^sub>s \<theta> \<notin> D" using 0[OF \<sigma>] by (metis subst_pair_compose)
moreover have "f \<cdot>\<^sub>p \<delta> \<in> set (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
using f(1) by (auto simp add: subst_apply_pairs_def)
ultimately have "list_ex (\<lambda>f. f \<cdot>\<^sub>p \<sigma> \<circ>\<^sub>s \<theta> \<notin> D) (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
using f(1) Bex_set by fastforce
} moreover {
fix \<sigma>::"('a,'b) subst" and t t'
assume \<sigma>: "subst_domain \<sigma> = set X" "ground (subst_range \<sigma>)"
and *: "list_ex (\<lambda>f. fst f \<cdot> (\<sigma> \<circ>\<^sub>s \<theta>) \<noteq> snd f \<cdot> (\<sigma> \<circ>\<^sub>s \<theta>)) (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
obtain f where f: "f \<in> set (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)" "fst f \<cdot> \<sigma> \<circ>\<^sub>s \<theta> \<noteq> snd f \<cdot> \<sigma> \<circ>\<^sub>s \<theta>"
using * by (induct F) (auto simp add: subst_apply_pairs_def)
then obtain g where g: "g \<in> set F" "f = g \<cdot>\<^sub>p \<delta>" by (auto simp add: subst_apply_pairs_def)
have "fst g \<cdot> \<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) \<noteq> snd g \<cdot> \<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>)"
using f(2) g 0[OF \<sigma>] by (simp add: prod.case_eq_if)
hence "list_ex (\<lambda>f. fst f \<cdot> (\<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>)) \<noteq> snd f \<cdot> (\<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>))) F"
using g Bex_set by fastforce
} moreover {
fix \<sigma>::"('a,'b) subst" and t t'
assume \<sigma>: "subst_domain \<sigma> = set X" "ground (subst_range \<sigma>)"
and *: "list_ex (\<lambda>f. f \<cdot>\<^sub>p (\<sigma> \<circ>\<^sub>s \<theta>) \<notin> D) (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
obtain f where f: "f \<in> set (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)" "f \<cdot>\<^sub>p \<sigma> \<circ>\<^sub>s \<theta> \<notin> D"
using * by (induct F') (auto simp add: subst_apply_pairs_def)
then obtain g where g: "g \<in> set F'" "f = g \<cdot>\<^sub>p \<delta>" by (auto simp add: subst_apply_pairs_def)
have "g \<cdot>\<^sub>p \<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) \<notin> D"
using f(2) g 0[OF \<sigma>] by (simp add: prod.case_eq_if)
hence "list_ex (\<lambda>f. f \<cdot>\<^sub>p (\<sigma> \<circ>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>)) \<notin> D) F'"
using g Bex_set by fastforce
} ultimately show ?thesis using assms unfolding negchecks_model_def by blast
qed
lemma strand_sem_subst_stateful:
fixes \<delta>::"('fun,'var) subst"
assumes "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> bvars\<^sub>s\<^sub>s\<^sub>t S = {}"
shows "\<lbrakk>M; D; S\<rbrakk>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) \<longleftrightarrow> \<lbrakk>M; D; S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>s \<theta>"
proof
note [simp] = subst_sst_cons[of _ _ \<delta>] subst_subst_compose[of _ \<delta> \<theta>]
have "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> (subst_domain \<gamma> \<union> range_vars \<gamma>) = {}"
when \<delta>: "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> set X = {}"
and \<gamma>: "subst_domain \<gamma> = set X" "ground (subst_range \<gamma>)"
for X and \<gamma>::"('fun,'var) subst"
using \<delta> \<gamma> unfolding range_vars_alt_def by auto
hence 0: "\<gamma> \<circ>\<^sub>s \<delta> = \<delta> \<circ>\<^sub>s \<gamma>"
when \<delta>: "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> set X = {}"
and \<gamma>: "subst_domain \<gamma> = set X" "ground (subst_range \<gamma>)"
for \<gamma> X
by (metis \<delta> \<gamma> subst_comp_eq_if_disjoint_vars)
show "\<lbrakk>M; D; S\<rbrakk>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>) \<Longrightarrow> \<lbrakk>M; D; S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>s \<theta>" using assms
proof (induction S arbitrary: M D rule: strand_sem_stateful_induct)
case (ConsNegChecks M D X F F' S)
hence *: "\<lbrakk>M; D; S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>s \<theta>" and **: "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> set X = {}"
unfolding bvars\<^sub>s\<^sub>s\<^sub>t_def negchecks_model_def by (force, auto)
have "negchecks_model (\<delta> \<circ>\<^sub>s \<theta>) D X F F'" using ConsNegChecks by auto
hence "negchecks_model \<theta> D X (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>) (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
using 0[OF **] negchecks_model_subst[OF **] by blast
moreover have "rm_vars (set X) \<delta> = \<delta>" using ConsNegChecks.prems(2) by force
ultimately show ?case using * by auto
qed simp_all
show "\<lbrakk>M; D; S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>s \<theta> \<Longrightarrow> \<lbrakk>M; D; S\<rbrakk>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>)" using assms
proof (induction S arbitrary: M D rule: strand_sem_stateful_induct)
case (ConsNegChecks M D X F F' S)
have \<delta>: "rm_vars (set X) \<delta> = \<delta>" using ConsNegChecks.prems(2) by force
hence *: "\<lbrakk>M; D; S\<rbrakk>\<^sub>s (\<delta> \<circ>\<^sub>s \<theta>)" and **: "(subst_domain \<delta> \<union> range_vars \<delta>) \<inter> set X = {}"
using ConsNegChecks unfolding bvars\<^sub>s\<^sub>s\<^sub>t_def negchecks_model_def by auto
have "negchecks_model \<theta> D X (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>) (F' \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s \<delta>)"
using ConsNegChecks.prems(1) \<delta> by (auto simp add: subst_compose_assoc negchecks_model_def)
hence "negchecks_model (\<delta> \<circ>\<^sub>s \<theta>) D X F F'"
using 0[OF **] negchecks_model_subst[OF **] by blast
thus ?case using * by auto
qed simp_all
qed
end
subsection \<open>Well-Formedness Lemmata\<close>
lemma wfvarsocc\<^sub>s\<^sub>s\<^sub>t_subset_wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t[simp]:
"wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S \<subseteq> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S"
by (induction S)
(auto simp add: wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def
split: stateful_strand_step.split poscheckvariant.split)
lemma wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_append: "wfvarsoccs\<^sub>s\<^sub>s\<^sub>t (S@S') = wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S \<union> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S'"
by (simp add: wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def)
lemma wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_union[simp]:
"wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t (S@T) = wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<union> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t T"
by (simp add: wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def)
lemma wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_singleton:
"wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t [s] = wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t\<^sub>p s"
by (simp add: wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def)
lemma wf\<^sub>s\<^sub>s\<^sub>t_prefix[dest]: "wf'\<^sub>s\<^sub>s\<^sub>t V (S@S') \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t V S"
by (induct S rule: wf'\<^sub>s\<^sub>s\<^sub>t.induct) auto
lemma wf\<^sub>s\<^sub>s\<^sub>t_vars_mono: "wf'\<^sub>s\<^sub>s\<^sub>t V S \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> W) S"
proof (induction S arbitrary: V)
case (Cons x S) thus ?case
proof (cases x)
case (Send t)
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> W) S" using Cons.prems(1) Cons.IH by simp
thus ?thesis using Send by (simp add: sup_commute sup_left_commute)
next
case (Equality a t t')
show ?thesis
proof (cases a)
case Assign
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> W) S" "fv t' \<subseteq> V \<union> W" using Equality Cons.prems(1) Cons.IH by auto
thus ?thesis using Equality Assign by (simp add: sup_commute sup_left_commute)
next
case Check thus ?thesis using Equality Cons by auto
qed
next
case (InSet a t t')
show ?thesis
proof (cases a)
case Assign
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> fv t' \<union> W) S" using InSet Cons.prems(1) Cons.IH by auto
thus ?thesis using InSet Assign by (simp add: sup_commute sup_left_commute)
next
case Check thus ?thesis using InSet Cons by auto
qed
qed auto
qed simp
lemma wf\<^sub>s\<^sub>s\<^sub>tI[intro]: "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<subseteq> V \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t V S"
proof (induction S)
case (Cons x S) thus ?case
proof (cases x)
case (Send t)
hence "wf'\<^sub>s\<^sub>s\<^sub>t V S" "V \<union> fv t = V"
using Cons
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def
by auto
thus ?thesis using Send by simp
next
case (Equality a t t')
show ?thesis
proof (cases a)
case Assign
hence "wf'\<^sub>s\<^sub>s\<^sub>t V S" "fv t' \<subseteq> V"
using Equality Cons
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def
by auto
thus ?thesis using wf\<^sub>s\<^sub>s\<^sub>t_vars_mono Equality Assign by simp
next
case Check
thus ?thesis
using Equality Cons
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def
by auto
qed
next
case (InSet a t t')
show ?thesis
proof (cases a)
case Assign
hence "wf'\<^sub>s\<^sub>s\<^sub>t V S" "fv t \<union> fv t' \<subseteq> V"
using InSet Cons
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def
by auto
thus ?thesis using wf\<^sub>s\<^sub>s\<^sub>t_vars_mono InSet Assign by (simp add: Un_assoc)
next
case Check
thus ?thesis
using InSet Cons
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def
by auto
qed
qed (simp_all add: wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def)
qed (simp add: wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def)
lemma wf\<^sub>s\<^sub>s\<^sub>tI'[intro]:
assumes "\<Union>((\<lambda>x. case x of
Receive t \<Rightarrow> fv t
| Equality Assign _ t' \<Rightarrow> fv t'
| Insert t t' \<Rightarrow> fv t \<union> fv t'
| _ \<Rightarrow> {}) ` set S) \<subseteq> V"
shows "wf'\<^sub>s\<^sub>s\<^sub>t V S"
using assms
proof (induction S)
case (Cons x S) thus ?case
proof (cases x)
case (Equality a t t')
thus ?thesis using Cons by (cases a) (auto simp add: wf\<^sub>s\<^sub>s\<^sub>t_vars_mono)
next
case (InSet a t t')
thus ?thesis using Cons by (cases a) (auto simp add: wf\<^sub>s\<^sub>s\<^sub>t_vars_mono Un_assoc)
qed (simp_all add: wf\<^sub>s\<^sub>s\<^sub>t_vars_mono)
qed simp
lemma wf\<^sub>s\<^sub>s\<^sub>t_append_exec: "wf'\<^sub>s\<^sub>s\<^sub>t V (S@S') \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S) S'"
proof (induction S arbitrary: V)
case (Cons x S V) thus ?case
proof (cases x)
case (Send t)
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S) S'" using Cons.prems Cons.IH by simp
thus ?thesis using Send unfolding wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def by (auto simp add: sup_assoc)
next
case (Equality a t t') show ?thesis
proof (cases a)
case Assign
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S) S'" using Equality Cons.prems Cons.IH by auto
thus ?thesis using Equality Assign unfolding wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def by (auto simp add: sup_assoc)
next
case Check
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S) S'" using Equality Cons.prems Cons.IH by auto
thus ?thesis using Equality Check unfolding wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def by (auto simp add: sup_assoc)
qed
next
case (InSet a t t') show ?thesis
proof (cases a)
case Assign
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> fv t' \<union> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S) S'" using InSet Cons.prems Cons.IH by auto
thus ?thesis using InSet Assign unfolding wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def by (auto simp add: sup_assoc)
next
case Check
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S) S'" using InSet Cons.prems Cons.IH by auto
thus ?thesis using InSet Check unfolding wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def by (auto simp add: sup_assoc)
qed
qed (auto simp add: wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def)
qed (simp add: wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def)
lemma wf\<^sub>s\<^sub>s\<^sub>t_append:
"wf'\<^sub>s\<^sub>s\<^sub>t X S \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t Y T \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t (X \<union> Y) (S@T)"
proof (induction X S rule: wf'\<^sub>s\<^sub>s\<^sub>t.induct)
case 1 thus ?case by (metis wf\<^sub>s\<^sub>s\<^sub>t_vars_mono Un_commute append_Nil)
next
case 3 thus ?case by (metis append_Cons Un_commute Un_assoc wf'\<^sub>s\<^sub>s\<^sub>t.simps(3))
next
case (4 V t t' S)
hence *: "fv t' \<subseteq> V" and "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> Y) (S @ T)" by simp_all
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> Y \<union> fv t) (S @ T)" by (metis Un_commute Un_assoc)
thus ?case using * by auto
next
case (8 V t t' S)
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> fv t' \<union> Y) (S @ T)" by simp_all
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> Y \<union> fv t \<union> fv t') (S @ T)" by (metis Un_commute Un_assoc)
thus ?case by auto
qed auto
lemma wf\<^sub>s\<^sub>s\<^sub>t_append_suffix:
"wf'\<^sub>s\<^sub>s\<^sub>t V S \<Longrightarrow> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<union> V \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t V (S@S')"
proof (induction V S rule: wf'\<^sub>s\<^sub>s\<^sub>t.induct)
case (2 V t S)
hence *: "fv t \<subseteq> V" "wf'\<^sub>s\<^sub>s\<^sub>t V S" by simp_all
hence "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<union> V"
using "2.prems"(2) unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def by auto
thus ?case using "2.IH" * by simp
next
case (3 V t S)
hence *: "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t) S" by simp_all
hence "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<union> (V \<union> fv t)"
using "3.prems"(2) unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def by auto
thus ?case using "3.IH" * by simp
next
case (4 V t t' S)
hence *: "fv t' \<subseteq> V" "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t) S" by simp_all
moreover have "vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (\<langle>t := t'\<rangle>) = fv t \<union> fv t'"
by simp
moreover have "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t (\<langle>t := t'\<rangle>#S) = fv t \<union> fv t' \<union> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S"
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def by auto
ultimately have "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<union> (V \<union> fv t)"
using "4.prems"(2) by blast
thus ?case using "4.IH" * by simp
next
case (6 V t t' S)
hence *: "fv t \<union> fv t' \<subseteq> V" "wf'\<^sub>s\<^sub>s\<^sub>t V S" by simp_all
moreover have "vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (insert\<langle>t,t'\<rangle>) = fv t \<union> fv t'"
by simp
moreover have "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t (insert\<langle>t,t'\<rangle>#S) = fv t \<union> fv t' \<union> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S"
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def by auto
ultimately have "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<union> V"
using "6.prems"(2) by blast
thus ?case using "6.IH" * by simp
next
case (8 V t t' S)
hence *: "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> fv t') S" by simp_all
moreover have "vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (select\<langle>t,t'\<rangle>) = fv t \<union> fv t'"
by simp
moreover have "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t (select\<langle>t,t'\<rangle>#S) = fv t \<union> fv t' \<union> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S"
unfolding wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def by auto
ultimately have "wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S' \<subseteq> wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t S \<union> (V \<union> fv t \<union> fv t')"
using "8.prems"(2) by blast
thus ?case using "8.IH" * by simp
qed (simp_all add: wf\<^sub>s\<^sub>s\<^sub>tI wfrestrictedvars\<^sub>s\<^sub>s\<^sub>t_def)
lemma wf\<^sub>s\<^sub>s\<^sub>t_append_suffix':
assumes "wf'\<^sub>s\<^sub>s\<^sub>t V S"
and "\<Union>((\<lambda>x. case x of
Receive t \<Rightarrow> fv t
| Equality Assign _ t' \<Rightarrow> fv t'
| Insert t t' \<Rightarrow> fv t \<union> fv t'
| _ \<Rightarrow> {}) ` set S') \<subseteq> wfvarsoccs\<^sub>s\<^sub>s\<^sub>t S \<union> V"
shows "wf'\<^sub>s\<^sub>s\<^sub>t V (S@S')"
using assms
by (induction V S rule: wf'\<^sub>s\<^sub>s\<^sub>t.induct)
(auto simp add: wf\<^sub>s\<^sub>s\<^sub>tI' wf\<^sub>s\<^sub>s\<^sub>t_vars_mono wfvarsoccs\<^sub>s\<^sub>s\<^sub>t_def)
lemma wf\<^sub>s\<^sub>s\<^sub>t_subst_apply:
"wf'\<^sub>s\<^sub>s\<^sub>t V S \<Longrightarrow> wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
proof (induction S arbitrary: V rule: wf'\<^sub>s\<^sub>s\<^sub>t.induct)
case (2 V t S)
hence "wf'\<^sub>s\<^sub>s\<^sub>t V S" "fv t \<subseteq> V" by simp_all
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)" "fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
using "2.IH" subst_apply_fv_subset by simp_all
thus ?case by (simp add: subst_apply_stateful_strand_def)
next
case (3 V t S)
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t) S" by simp
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> fv t))) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)" using "3.IH" by metis
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> fv (t \<cdot> \<delta>)) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)" by (metis subst_apply_fv_union)
thus ?case by (simp add: subst_apply_stateful_strand_def)
next
case (4 V t t' S)
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t) S" "fv t' \<subseteq> V" by auto
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> fv t))) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)" and *: "fv (t' \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
using "4.IH" subst_apply_fv_subset by force+
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> fv (t \<cdot> \<delta>)) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)" by (metis subst_apply_fv_union)
thus ?case using * by (simp add: subst_apply_stateful_strand_def)
next
case (6 V t t' S)
hence "wf'\<^sub>s\<^sub>s\<^sub>t V S" "fv t \<union> fv t' \<subseteq> V" by auto
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)" "fv (t \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)" "fv (t' \<cdot> \<delta>) \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
using "6.IH" subst_apply_fv_subset by force+
thus ?case by (simp add: sup_assoc subst_apply_stateful_strand_def)
next
case (8 V t t' S)
hence "wf'\<^sub>s\<^sub>s\<^sub>t (V \<union> fv t \<union> fv t') S" by auto
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> fv t \<union> fv t'))) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)"
using "8.IH" subst_apply_fv_subset by force
hence "wf'\<^sub>s\<^sub>s\<^sub>t (fv\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> fv (t \<cdot> \<delta>) \<union> fv (t' \<cdot> \<delta>)) (S \<cdot>\<^sub>s\<^sub>s\<^sub>t \<delta>)" by (metis subst_apply_fv_union)
thus ?case by (simp add: subst_apply_stateful_strand_def)
qed (auto simp add: subst_apply_stateful_strand_def)
end