541 lines
23 KiB
Plaintext
541 lines
23 KiB
Plaintext
(*
|
|
(C) Copyright Andreas Viktor Hess, DTU, 2015-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: Messages.thy
|
|
Author: Andreas Viktor Hess, DTU
|
|
*)
|
|
|
|
section \<open>Protocol Messages as (First-Order) Terms\<close>
|
|
|
|
theory Messages
|
|
imports Miscellaneous "First_Order_Terms.Term"
|
|
begin
|
|
|
|
subsection \<open>Term-related definitions: subterms and free variables\<close>
|
|
abbreviation "the_Fun \<equiv> un_Fun1"
|
|
lemmas the_Fun_def = un_Fun1_def
|
|
|
|
fun subterms::"('a,'b) term \<Rightarrow> ('a,'b) terms" where
|
|
"subterms (Var x) = {Var x}"
|
|
| "subterms (Fun f T) = {Fun f T} \<union> (\<Union>t \<in> set T. subterms t)"
|
|
|
|
abbreviation subtermeq (infix "\<sqsubseteq>" 50) where "t' \<sqsubseteq> t \<equiv> (t' \<in> subterms t)"
|
|
abbreviation subterm (infix "\<sqsubset>" 50) where "t' \<sqsubset> t \<equiv> (t' \<sqsubseteq> t \<and> t' \<noteq> t)"
|
|
|
|
abbreviation "subterms\<^sub>s\<^sub>e\<^sub>t M \<equiv> \<Union>(subterms ` M)"
|
|
abbreviation subtermeqset (infix "\<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t" 50) where "t \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t M \<equiv> (t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M)"
|
|
|
|
abbreviation fv where "fv \<equiv> vars_term"
|
|
lemmas fv_simps = term.simps(17,18)
|
|
|
|
fun fv\<^sub>s\<^sub>e\<^sub>t where "fv\<^sub>s\<^sub>e\<^sub>t M = \<Union>(fv ` M)"
|
|
|
|
abbreviation fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r where "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r p \<equiv> case p of (t,t') \<Rightarrow> fv t \<union> fv t'"
|
|
|
|
fun fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s where "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F = \<Union>(fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r ` set F)"
|
|
|
|
abbreviation ground where "ground M \<equiv> fv\<^sub>s\<^sub>e\<^sub>t M = {}"
|
|
|
|
|
|
subsection \<open>Variants that return lists insteads of sets\<close>
|
|
fun fv_list where
|
|
"fv_list (Var x) = [x]"
|
|
| "fv_list (Fun f T) = concat (map fv_list T)"
|
|
|
|
definition fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s where
|
|
"fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<equiv> concat (map (\<lambda>(t,t'). fv_list t@fv_list t') F)"
|
|
|
|
fun subterms_list::"('a,'b) term \<Rightarrow> ('a,'b) term list" where
|
|
"subterms_list (Var x) = [Var x]"
|
|
| "subterms_list (Fun f T) = remdups (Fun f T#concat (map subterms_list T))"
|
|
|
|
lemma fv_list_is_fv: "fv t = set (fv_list t)"
|
|
by (induct t) auto
|
|
|
|
lemma 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\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F = set (fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F)"
|
|
by (induct F) (auto simp add: fv_list_is_fv fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_def)
|
|
|
|
lemma subterms_list_is_subterms: "subterms t = set (subterms_list t)"
|
|
by (induct t) auto
|
|
|
|
|
|
subsection \<open>The subterm relation defined as a function\<close>
|
|
fun subterm_of where
|
|
"subterm_of t (Var y) = (t = Var y)"
|
|
| "subterm_of t (Fun f T) = (t = Fun f T \<or> list_ex (subterm_of t) T)"
|
|
|
|
lemma subterm_of_iff_subtermeq[code_unfold]: "t \<sqsubseteq> t' = subterm_of t t'"
|
|
proof (induction t')
|
|
case (Fun f T) thus ?case
|
|
proof (cases "t = Fun f T")
|
|
case False thus ?thesis
|
|
using Fun.IH subterm_of.simps(2)[of t f T]
|
|
unfolding list_ex_iff by fastforce
|
|
qed simp
|
|
qed simp
|
|
|
|
lemma subterm_of_ex_set_iff_subtermeqset[code_unfold]: "t \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t M = (\<exists>t' \<in> M. subterm_of t t')"
|
|
using subterm_of_iff_subtermeq by blast
|
|
|
|
|
|
subsection \<open>The subterm relation is a partial order on terms\<close>
|
|
|
|
interpretation "term": ordering "(\<sqsubseteq>)" "(\<sqsubset>)"
|
|
proof
|
|
show "s \<sqsubseteq> s" for s :: "('a,'b) term"
|
|
by (induct s rule: subterms.induct) auto
|
|
|
|
show trans: "s \<sqsubseteq> t \<Longrightarrow> t \<sqsubseteq> u \<Longrightarrow> s \<sqsubseteq> u" for s t u :: "('a,'b) term"
|
|
by (induct u rule: subterms.induct) auto
|
|
|
|
show "s \<sqsubseteq> t \<Longrightarrow> t \<sqsubseteq> s \<Longrightarrow> s = t" for s t :: "('a,'b) term"
|
|
proof (induction s arbitrary: t rule: subterms.induct[case_names Var Fun])
|
|
case (Fun f T)
|
|
{ assume 0: "t \<noteq> Fun f T"
|
|
then obtain u::"('a,'b) term" where u: "u \<in> set T" "t \<sqsubseteq> u" using Fun.prems(2) by auto
|
|
hence 1: "Fun f T \<sqsubseteq> u" using trans[OF Fun.prems(1)] by simp
|
|
|
|
have 2: "u \<sqsubseteq> Fun f T"
|
|
by (cases u) (use u(1) in force, use u(1) subterms.simps(2)[of f T] in fastforce)
|
|
hence 3: "u = Fun f T" using Fun.IH[OF u(1) _ 1] by simp
|
|
|
|
have "u \<sqsubseteq> t" using trans[OF 2 Fun.prems(1)] by simp
|
|
hence 4: "u = t" using Fun.IH[OF u(1) _ u(2)] by simp
|
|
|
|
have "t = Fun f T" using 3 4 by simp
|
|
hence False using 0 by simp
|
|
}
|
|
thus ?case by auto
|
|
qed simp
|
|
show \<open>s \<sqsubset> t \<longleftrightarrow> s \<sqsubset> t\<close> for s t :: "('a,'b) term" ..
|
|
qed
|
|
|
|
interpretation "term": order "(\<sqsubseteq>)" "(\<sqsubset>)"
|
|
by (rule ordering_orderI) (fact term.ordering_axioms)
|
|
|
|
subsection \<open>Lemmata concerning subterms and free variables\<close>
|
|
lemma fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_append: "fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F@G) = fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F@fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G"
|
|
by (simp add: fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_def)
|
|
|
|
lemma distinct_fv_list_idx_fv_disjoint:
|
|
assumes t: "distinct (fv_list t)" "Fun f T \<sqsubseteq> t"
|
|
and ij: "i < length T" "j < length T" "i < j"
|
|
shows "fv (T ! i) \<inter> fv (T ! j) = {}"
|
|
using t
|
|
proof (induction t rule: fv_list.induct)
|
|
case (2 g S)
|
|
have "distinct (fv_list s)" when s: "s \<in> set S" for s
|
|
by (metis (no_types, lifting) s "2.prems"(1) concat_append distinct_append
|
|
map_append split_list fv_list.simps(2) concat.simps(2) list.simps(9))
|
|
hence IH: "fv (T ! i) \<inter> fv (T ! j) = {}"
|
|
when s: "s \<in> set S" "Fun f T \<sqsubseteq> s" for s
|
|
using "2.IH" s by blast
|
|
|
|
show ?case
|
|
proof (cases "Fun f T = Fun g S")
|
|
case True
|
|
define U where "U \<equiv> map fv_list T"
|
|
|
|
have a: "distinct (concat U)"
|
|
using "2.prems"(1) True unfolding U_def by auto
|
|
|
|
have b: "i < length U" "j < length U"
|
|
using ij(1,2) unfolding U_def by simp_all
|
|
|
|
show ?thesis
|
|
using b distinct_concat_idx_disjoint[OF a b ij(3)]
|
|
fv_list_is_fv[of "T ! i"] fv_list_is_fv[of "T ! j"]
|
|
unfolding U_def by force
|
|
qed (use IH "2.prems"(2) in auto)
|
|
qed force
|
|
|
|
lemmas subtermeqI'[intro] = term.eq_refl
|
|
|
|
lemma subtermeqI''[intro]: "t \<in> set T \<Longrightarrow> t \<sqsubseteq> Fun f T"
|
|
by force
|
|
|
|
lemma finite_fv_set[intro]: "finite M \<Longrightarrow> finite (fv\<^sub>s\<^sub>e\<^sub>t M)"
|
|
by auto
|
|
|
|
lemma finite_fun_symbols[simp]: "finite (funs_term t)"
|
|
by (induct t) simp_all
|
|
|
|
lemma fv_set_mono: "M \<subseteq> N \<Longrightarrow> fv\<^sub>s\<^sub>e\<^sub>t M \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t N"
|
|
by auto
|
|
|
|
lemma subterms\<^sub>s\<^sub>e\<^sub>t_mono: "M \<subseteq> N \<Longrightarrow> subterms\<^sub>s\<^sub>e\<^sub>t M \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t N"
|
|
by auto
|
|
|
|
lemma ground_empty[simp]: "ground {}"
|
|
by simp
|
|
|
|
lemma ground_subset: "M \<subseteq> N \<Longrightarrow> ground N \<Longrightarrow> ground M"
|
|
by auto
|
|
|
|
lemma fv_map_fv_set: "\<Union>(set (map fv L)) = fv\<^sub>s\<^sub>e\<^sub>t (set L)"
|
|
by (induct L) auto
|
|
|
|
lemma fv\<^sub>s\<^sub>e\<^sub>t_union: "fv\<^sub>s\<^sub>e\<^sub>t (M \<union> N) = fv\<^sub>s\<^sub>e\<^sub>t M \<union> fv\<^sub>s\<^sub>e\<^sub>t N"
|
|
by auto
|
|
|
|
lemma finite_subset_Union:
|
|
fixes A::"'a set" and f::"'a \<Rightarrow> 'b set"
|
|
assumes "finite (\<Union>a \<in> A. f a)"
|
|
shows "\<exists>B. finite B \<and> B \<subseteq> A \<and> (\<Union>b \<in> B. f b) = (\<Union>a \<in> A. f a)"
|
|
by (metis assms eq_iff finite_subset_image finite_UnionD)
|
|
|
|
lemma inv_set_fv: "finite M \<Longrightarrow> \<Union>(set (map fv (inv set M))) = fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
using fv_map_fv_set[of "inv set M"] inv_set_fset by auto
|
|
|
|
lemma ground_subterm: "fv t = {} \<Longrightarrow> t' \<sqsubseteq> t \<Longrightarrow> fv t' = {}" by (induct t) auto
|
|
|
|
lemma empty_fv_not_var: "fv t = {} \<Longrightarrow> t \<noteq> Var x" by auto
|
|
|
|
lemma empty_fv_exists_fun: "fv t = {} \<Longrightarrow> \<exists>f X. t = Fun f X" by (cases t) auto
|
|
|
|
lemma vars_iff_subtermeq: "x \<in> fv t \<longleftrightarrow> Var x \<sqsubseteq> t" by (induct t) auto
|
|
|
|
lemma vars_iff_subtermeq_set: "x \<in> fv\<^sub>s\<^sub>e\<^sub>t M \<longleftrightarrow> Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t M"
|
|
using vars_iff_subtermeq[of x] by auto
|
|
|
|
lemma vars_if_subtermeq_set: "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> x \<in> fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
by (metis vars_iff_subtermeq_set)
|
|
|
|
lemma subtermeq_set_if_vars: "x \<in> fv\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t M"
|
|
by (metis vars_iff_subtermeq_set)
|
|
|
|
lemma vars_iff_subterm_or_eq: "x \<in> fv t \<longleftrightarrow> Var x \<sqsubset> t \<or> Var x = t"
|
|
by (induct t) (auto simp add: vars_iff_subtermeq)
|
|
|
|
lemma var_is_subterm: "x \<in> fv t \<Longrightarrow> Var x \<in> subterms t"
|
|
by (simp add: vars_iff_subtermeq)
|
|
|
|
lemma subterm_is_var: "Var x \<in> subterms t \<Longrightarrow> x \<in> fv t"
|
|
by (simp add: vars_iff_subtermeq)
|
|
|
|
lemma no_var_subterm: "\<not>t \<sqsubset> Var v" by auto
|
|
|
|
lemma fun_if_subterm: "t \<sqsubset> u \<Longrightarrow> \<exists>f X. u = Fun f X" by (induct u) simp_all
|
|
|
|
lemma subtermeq_vars_subset: "M \<sqsubseteq> N \<Longrightarrow> fv M \<subseteq> fv N" by (induct N) auto
|
|
|
|
lemma fv_subterms[simp]: "fv\<^sub>s\<^sub>e\<^sub>t (subterms t) = fv t"
|
|
by (induct t) auto
|
|
|
|
lemma fv_subterms_set[simp]: "fv\<^sub>s\<^sub>e\<^sub>t (subterms\<^sub>s\<^sub>e\<^sub>t M) = fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
using subtermeq_vars_subset by auto
|
|
|
|
lemma fv_subset: "t \<in> M \<Longrightarrow> fv t \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
by auto
|
|
|
|
lemma fv_subset_subterms: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> fv t \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t M"
|
|
using fv_subset fv_subterms_set by metis
|
|
|
|
lemma subterms_finite[simp]: "finite (subterms t)" by (induction rule: subterms.induct) auto
|
|
|
|
lemma subterms_union_finite: "finite M \<Longrightarrow> finite (\<Union>t \<in> M. subterms t)"
|
|
by (induction rule: subterms.induct) auto
|
|
|
|
lemma subterms_subset: "t' \<sqsubseteq> t \<Longrightarrow> subterms t' \<subseteq> subterms t"
|
|
by (induction rule: subterms.induct) auto
|
|
|
|
lemma subterms_subset_set: "M \<subseteq> subterms t \<Longrightarrow> subterms\<^sub>s\<^sub>e\<^sub>t M \<subseteq> subterms t"
|
|
by (metis SUP_least contra_subsetD subterms_subset)
|
|
|
|
lemma subset_subterms_Union[simp]: "M \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t M" by auto
|
|
|
|
lemma in_subterms_Union: "t \<in> M \<Longrightarrow> t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M" using subset_subterms_Union by blast
|
|
|
|
lemma in_subterms_subset_Union: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> subterms t \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t M"
|
|
using subterms_subset by auto
|
|
|
|
lemma subterm_param_split:
|
|
assumes "t \<sqsubset> Fun f X"
|
|
shows "\<exists>pre x suf. t \<sqsubseteq> x \<and> X = pre@x#suf"
|
|
proof -
|
|
obtain x where "t \<sqsubseteq> x" "x \<in> set X" using assms by auto
|
|
then obtain pre suf where "X = pre@x#suf" "x \<notin> set pre \<or> x \<notin> set suf"
|
|
by (meson split_list_first split_list_last)
|
|
thus ?thesis using \<open>t \<sqsubseteq> x\<close> by auto
|
|
qed
|
|
|
|
lemma ground_iff_no_vars: "ground (M::('a,'b) terms) \<longleftrightarrow> (\<forall>v. Var v \<notin> (\<Union>m \<in> M. subterms m))"
|
|
proof
|
|
assume "ground M"
|
|
hence "\<forall>v. \<forall>m \<in> M. v \<notin> fv m" by auto
|
|
hence "\<forall>v. \<forall>m \<in> M. Var v \<notin> subterms m" by (simp add: vars_iff_subtermeq)
|
|
thus "(\<forall>v. Var v \<notin> (\<Union>m \<in> M. subterms m))" by simp
|
|
next
|
|
assume no_vars: "\<forall>v. Var v \<notin> (\<Union>m \<in> M. subterms m)"
|
|
moreover
|
|
{ assume "\<not>ground M"
|
|
then obtain v and m::"('a,'b) term" where "m \<in> M" "fv m \<noteq> {}" "v \<in> fv m" by auto
|
|
hence "Var v \<in> (subterms m)" by (simp add: vars_iff_subtermeq)
|
|
hence "\<exists>v. Var v \<in> (\<Union>t \<in> M. subterms t)" using \<open>m \<in> M\<close> by auto
|
|
hence False using no_vars by simp
|
|
}
|
|
ultimately show "ground M" by blast
|
|
qed
|
|
|
|
lemma index_Fun_subterms_subset[simp]: "i < length T \<Longrightarrow> subterms (T ! i) \<subseteq> subterms (Fun f T)"
|
|
by auto
|
|
|
|
lemma index_Fun_fv_subset[simp]: "i < length T \<Longrightarrow> fv (T ! i) \<subseteq> fv (Fun f T)"
|
|
using subtermeq_vars_subset by fastforce
|
|
|
|
lemma subterms_union_ground:
|
|
assumes "ground M"
|
|
shows "ground (subterms\<^sub>s\<^sub>e\<^sub>t M)"
|
|
proof -
|
|
{ fix t assume "t \<in> M"
|
|
hence "fv t = {}"
|
|
using ground_iff_no_vars[of M] assms
|
|
by auto
|
|
hence "\<forall>t' \<in> subterms t. fv t' = {}" using subtermeq_vars_subset[of _ t] by simp
|
|
hence "ground (subterms t)" by auto
|
|
}
|
|
thus ?thesis by auto
|
|
qed
|
|
|
|
lemma Var_subtermeq: "t \<sqsubseteq> Var v \<Longrightarrow> t = Var v" by simp
|
|
|
|
lemma subtermeq_imp_funs_term_subset: "s \<sqsubseteq> t \<Longrightarrow> funs_term s \<subseteq> funs_term t"
|
|
by (induct t arbitrary: s) auto
|
|
|
|
lemma subterms_const: "subterms (Fun f []) = {Fun f []}" by simp
|
|
|
|
lemma subterm_subtermeq_neq: "\<lbrakk>t \<sqsubset> u; u \<sqsubseteq> v\<rbrakk> \<Longrightarrow> t \<noteq> v"
|
|
by (metis term.eq_iff)
|
|
|
|
lemma subtermeq_subterm_neq: "\<lbrakk>t \<sqsubseteq> u; u \<sqsubset> v\<rbrakk> \<Longrightarrow> t \<noteq> v"
|
|
by (metis term.eq_iff)
|
|
|
|
lemma subterm_size_lt: "x \<sqsubset> y \<Longrightarrow> size x < size y"
|
|
using not_less_eq size_list_estimation by (induct y, simp, fastforce)
|
|
|
|
lemma in_subterms_eq: "\<lbrakk>x \<in> subterms y; y \<in> subterms x\<rbrakk> \<Longrightarrow> subterms x = subterms y"
|
|
using term.antisym by auto
|
|
|
|
lemma Fun_gt_params: "Fun f X \<notin> (\<Union>x \<in> set X. subterms x)"
|
|
proof -
|
|
have "size_list size X < size (Fun f X)" by simp
|
|
hence "Fun f X \<notin> set X" by (meson less_not_refl size_list_estimation)
|
|
hence "\<forall>x \<in> set X. Fun f X \<notin> subterms x \<or> x \<notin> subterms (Fun f X)"
|
|
by (metis term.antisym[of "Fun f X" _])
|
|
moreover have "\<forall>x \<in> set X. x \<in> subterms (Fun f X)" by fastforce
|
|
ultimately show ?thesis by auto
|
|
qed
|
|
|
|
lemma params_subterms[simp]: "set X \<subseteq> subterms (Fun f X)" by auto
|
|
|
|
lemma params_subterms_Union[simp]: "subterms\<^sub>s\<^sub>e\<^sub>t (set X) \<subseteq> subterms (Fun f X)" by auto
|
|
|
|
lemma Fun_subterm_inside_params: "t \<sqsubset> Fun f X \<longleftrightarrow> t \<in> (\<Union>x \<in> (set X). subterms x)"
|
|
using Fun_gt_params by fastforce
|
|
|
|
lemma Fun_param_is_subterm: "x \<in> set X \<Longrightarrow> x \<sqsubset> Fun f X"
|
|
using Fun_subterm_inside_params by fastforce
|
|
|
|
lemma Fun_param_in_subterms: "x \<in> set X \<Longrightarrow> x \<in> subterms (Fun f X)"
|
|
using Fun_subterm_inside_params by fastforce
|
|
|
|
lemma Fun_not_in_param: "x \<in> set X \<Longrightarrow> \<not>Fun f X \<sqsubset> x"
|
|
using term.antisym by fast
|
|
|
|
lemma Fun_ex_if_subterm: "t \<sqsubset> s \<Longrightarrow> \<exists>f T. Fun f T \<sqsubseteq> s \<and> t \<in> set T"
|
|
proof (induction s)
|
|
case (Fun f T)
|
|
then obtain s' where s': "s' \<in> set T" "t \<sqsubseteq> s'" by auto
|
|
show ?case
|
|
proof (cases "t = s'")
|
|
case True thus ?thesis using s' by blast
|
|
next
|
|
case False
|
|
thus ?thesis
|
|
using Fun.IH[OF s'(1)] s'(2) term.order_trans[OF _ Fun_param_in_subterms[OF s'(1), of f]]
|
|
by metis
|
|
qed
|
|
qed simp
|
|
|
|
lemma const_subterm_obtain:
|
|
assumes "fv t = {}"
|
|
obtains c where "Fun c [] \<sqsubseteq> t"
|
|
using assms
|
|
proof (induction t)
|
|
case (Fun f T) thus ?case by (cases "T = []") force+
|
|
qed simp
|
|
|
|
lemma const_subterm_obtain': "fv t = {} \<Longrightarrow> \<exists>c. Fun c [] \<sqsubseteq> t"
|
|
by (metis const_subterm_obtain)
|
|
|
|
lemma subterms_singleton:
|
|
assumes "(\<exists>v. t = Var v) \<or> (\<exists>f. t = Fun f [])"
|
|
shows "subterms t = {t}"
|
|
using assms by (cases t) auto
|
|
|
|
lemma subtermeq_Var_const:
|
|
assumes "s \<sqsubseteq> t"
|
|
shows "t = Var v \<Longrightarrow> s = Var v" "t = Fun f [] \<Longrightarrow> s = Fun f []"
|
|
using assms by fastforce+
|
|
|
|
lemma subterms_singleton':
|
|
assumes "subterms t = {t}"
|
|
shows "(\<exists>v. t = Var v) \<or> (\<exists>f. t = Fun f [])"
|
|
proof (cases t)
|
|
case (Fun f T)
|
|
{ fix s S assume "T = s#S"
|
|
hence "s \<in> subterms t" using Fun by auto
|
|
hence "s = t" using assms by auto
|
|
hence False
|
|
using Fun_param_is_subterm[of s "s#S" f] \<open>T = s#S\<close> Fun
|
|
by auto
|
|
}
|
|
hence "T = []" by (cases T) auto
|
|
thus ?thesis using Fun by simp
|
|
qed (simp add: assms)
|
|
|
|
lemma funs_term_subterms_eq[simp]:
|
|
"(\<Union>s \<in> subterms t. funs_term s) = funs_term t"
|
|
"(\<Union>s \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. funs_term s) = \<Union>(funs_term ` M)"
|
|
proof -
|
|
show "\<And>t. \<Union>(funs_term ` subterms t) = funs_term t"
|
|
using term.order_refl subtermeq_imp_funs_term_subset by blast
|
|
thus "\<Union>(funs_term ` (subterms\<^sub>s\<^sub>e\<^sub>t M)) = \<Union>(funs_term ` M)" by force
|
|
qed
|
|
|
|
lemmas subtermI'[intro] = Fun_param_is_subterm
|
|
|
|
lemma funs_term_Fun_subterm: "f \<in> funs_term t \<Longrightarrow> \<exists>T. Fun f T \<in> subterms t"
|
|
proof (induction t)
|
|
case (Fun g T)
|
|
hence "f = g \<or> (\<exists>s \<in> set T. f \<in> funs_term s)" by simp
|
|
thus ?case
|
|
proof
|
|
assume "\<exists>s \<in> set T. f \<in> funs_term s"
|
|
then obtain s where "s \<in> set T" "\<exists>T. Fun f T \<in> subterms s" using Fun.IH by auto
|
|
thus ?thesis by auto
|
|
qed (auto simp add: Fun)
|
|
qed simp
|
|
|
|
lemma funs_term_Fun_subterm': "Fun f T \<in> subterms t \<Longrightarrow> f \<in> funs_term t"
|
|
by (induct t) auto
|
|
|
|
lemma zip_arg_subterm:
|
|
assumes "(s,t) \<in> set (zip X Y)"
|
|
shows "s \<sqsubset> Fun f X" "t \<sqsubset> Fun g Y"
|
|
proof -
|
|
from assms have *: "s \<in> set X" "t \<in> set Y" by (meson in_set_zipE)+
|
|
show "s \<sqsubset> Fun f X" by (metis Fun_param_is_subterm[OF *(1)])
|
|
show "t \<sqsubset> Fun g Y" by (metis Fun_param_is_subterm[OF *(2)])
|
|
qed
|
|
|
|
lemma fv_disj_Fun_subterm_param_cases:
|
|
assumes "fv t \<inter> X = {}" "Fun f T \<in> subterms t"
|
|
shows "T = [] \<or> (\<exists>s\<in>set T. s \<notin> Var ` X)"
|
|
proof (cases T)
|
|
case (Cons s S)
|
|
hence "s \<in> subterms t"
|
|
using assms(2) term.order_trans[of _ "Fun f T" t]
|
|
by auto
|
|
hence "fv s \<inter> X = {}" using assms(1) fv_subterms by force
|
|
thus ?thesis using Cons by auto
|
|
qed simp
|
|
|
|
lemma fv_eq_FunI:
|
|
assumes "length T = length S" "\<And>i. i < length T \<Longrightarrow> fv (T ! i) = fv (S ! i)"
|
|
shows "fv (Fun f T) = fv (Fun g S)"
|
|
using assms
|
|
proof (induction T arbitrary: S)
|
|
case (Cons t T S')
|
|
then obtain s S where S': "S' = s#S" by (cases S') simp_all
|
|
thus ?case using Cons by fastforce
|
|
qed simp
|
|
|
|
lemma fv_eq_FunI':
|
|
assumes "length T = length S" "\<And>i. i < length T \<Longrightarrow> x \<in> fv (T ! i) \<longleftrightarrow> x \<in> fv (S ! i)"
|
|
shows "x \<in> fv (Fun f T) \<longleftrightarrow> x \<in> fv (Fun g S)"
|
|
using assms
|
|
proof (induction T arbitrary: S)
|
|
case (Cons t T S')
|
|
then obtain s S where S': "S' = s#S" by (cases S') simp_all
|
|
thus ?case using Cons by fastforce
|
|
qed simp
|
|
|
|
lemma finite_fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s[simp]: "finite (fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s x)" by auto
|
|
|
|
lemma fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_Nil[simp]: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s [] = {}" by simp
|
|
|
|
lemma fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_singleton[simp]: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s [(t,s)] = fv t \<union> fv s" by simp
|
|
|
|
lemma fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_Cons: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ((s,t)#F) = fv s \<union> fv t \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F" by simp
|
|
|
|
lemma fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_append: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F@G) = 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
|
|
|
|
lemma fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_mono: "set M \<subseteq> set N \<Longrightarrow> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s M \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s N" by auto
|
|
|
|
lemma fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_inI[intro]:
|
|
"f \<in> set F \<Longrightarrow> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r f \<Longrightarrow> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F"
|
|
"f \<in> set F \<Longrightarrow> x \<in> fv (fst f) \<Longrightarrow> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F"
|
|
"f \<in> set F \<Longrightarrow> x \<in> fv (snd f) \<Longrightarrow> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F"
|
|
"(t,s) \<in> set F \<Longrightarrow> x \<in> fv t \<Longrightarrow> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F"
|
|
"(t,s) \<in> set F \<Longrightarrow> x \<in> fv s \<Longrightarrow> x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F"
|
|
using UN_I by fastforce+
|
|
|
|
lemma fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_cons_subset: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (f#F)"
|
|
by auto
|
|
|
|
|
|
subsection \<open>Other lemmata\<close>
|
|
lemma nonvar_term_has_composed_shallow_term:
|
|
fixes t::"('f,'v) term"
|
|
assumes "\<not>(\<exists>x. t = Var x)"
|
|
shows "\<exists>f T. Fun f T \<sqsubseteq> t \<and> (\<forall>s \<in> set T. (\<exists>c. s = Fun c []) \<or> (\<exists>x. s = Var x))"
|
|
proof -
|
|
let ?Q = "\<lambda>S. \<forall>s \<in> set S. (\<exists>c. s = Fun c []) \<or> (\<exists>x. s = Var x)"
|
|
let ?P = "\<lambda>t. \<exists>g S. Fun g S \<sqsubseteq> t \<and> ?Q S"
|
|
{ fix t::"('f,'v) term"
|
|
have "(\<exists>x. t = Var x) \<or> ?P t"
|
|
proof (induction t)
|
|
case (Fun h R) show ?case
|
|
proof (cases "R = [] \<or> (\<forall>r \<in> set R. \<exists>x. r = Var x)")
|
|
case False
|
|
then obtain r g S where "r \<in> set R" "?P r" "Fun g S \<sqsubseteq> r" "?Q S" using Fun.IH by fast
|
|
thus ?thesis by auto
|
|
qed force
|
|
qed simp
|
|
} thus ?thesis using assms by blast
|
|
qed
|
|
|
|
end
|