(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2018

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

    These theories depend on the IsaFoR library v2.27 available at:
    http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/23ac5f5c26ed
    Download into the directory IsaFoR and move it to your Isabelle installation or change the path in the imports.
*)

section {* Theory: Messages *}
theory Messages
imports Main "~~/src/HOL/Library/Countable_Set"
        "~~/IsaFoR/thys/Rewriting/Term" (* Path to IsaFoR *)
begin

subsection {* Term-related definitions *}
instance "term" :: (countable, countable) countable
by countable_datatype

fun subterms::"('a,'b) term \<Rightarrow> ('a,'b) terms" where
  "subterms (Var x) = {Var x}"
| "subterms (Fun f X) = {Fun f X} \<union> (\<Union>x \<in> (set X). subterms x)"

definition subtermeq (infix "\<sqsubseteq>" 50) where "t' \<sqsubseteq> t \<equiv> (t' \<in> subterms t)"
definition subterm (infix "\<sqsubset>" 50) where "t' \<sqsubset> t \<equiv> (t' \<sqsubseteq> t \<and> t' \<noteq> t)"

abbreviation FV where "FV \<equiv> vars_term"
lemmas FV_simps = term.simps(17,18)

definition FV\<^sub>s\<^sub>e\<^sub>t where "FV\<^sub>s\<^sub>e\<^sub>t M \<equiv> (\<Union>m \<in> M. FV m)"
definition ground where "ground M \<equiv> FV\<^sub>s\<^sub>e\<^sub>t M = {}"

declare subtermeq_def[simp]
declare subterm_def[simp]
declare ground_def[simp]
declare FV\<^sub>s\<^sub>e\<^sub>t_def[simp]

lemma subtermD[dest]: "s \<sqsubset> t \<Longrightarrow> s \<lhd> t" "s \<sqsubseteq> t \<Longrightarrow> s \<unlhd> t" by (induct t) auto

lemma subterm_from_supt: "s \<lhd> t \<Longrightarrow> s \<sqsubset> t"
proof (induction s rule: supt.induct)
  case (arg s S f) thus ?case unfolding subterm_def subtermeq_def
    by (metis (mono_tags, hide_lams) UN_I UnCI insertCI is_FunE is_VarE
                                     subterms.simps(1,2) term_not_arg) 
next
  case (subt s S t f) thus ?case using supt_not_sym by fastforce
qed

lemma subtermeq_from_supteq: "s \<unlhd> t \<Longrightarrow> s \<sqsubseteq> t"
proof (induction s rule: supteq.induct)
  case (refl t) thus ?case by (cases t) auto
qed auto


subsection {* Lemmas concerning subterms and free variables *}
lemma in_subterms_refl[simp]: "t \<in> subterms t"
by (induct t rule: subterms.induct) auto

lemma subtermI[intro]: "x \<in> subterms y \<Longrightarrow> x \<noteq> y \<Longrightarrow> x \<sqsubset> y" by simp
lemma subtermI'[intro]: "x \<in> set X \<Longrightarrow> x \<sqsubset> Fun f X" by force
lemma subtermeqI[intro]: "x \<in> subterms y \<Longrightarrow> x \<sqsubseteq> y" by simp
lemma subtermeqI'[intro]: "x = y \<Longrightarrow> x \<sqsubseteq> y" using in_subterms_refl by simp
lemma subtermeqI''[intro]: "x \<in> set X \<Longrightarrow> x \<sqsubseteq> Fun f X" by force
lemma subtermeqD[dest]: "x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> x \<sqsubset> y" by simp

lemma subterms_UnionE:
  assumes "t \<in> \<Union>(subterms ` M)"
  obtains t' where "t' \<in> M" "t \<sqsubseteq> t'"
using assms by auto

lemma finite_FV[simp]: "finite (FV t)" by (induct t) simp_all
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_Union_mono: "M \<subseteq> N \<Longrightarrow> \<Union>(subterms ` M) \<subseteq> \<Union>(subterms ` N)" by auto

lemma inv_set_fset: "finite M \<Longrightarrow> set (inv set M) = M" 
unfolding inv_def by (metis (mono_tags) finite_list someI_ex)

lemma FV_map_FV_set: "\<Union>set (map FV L) = FV\<^sub>s\<^sub>e\<^sub>t (set L)" by (induct L) 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 Union_image_eq)

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 FV_Fun_cons: "FV (Fun f (x#X)) = FV x \<union> FV (Fun f X)" by auto

lemma ground_subterm: "FV t = {} \<Longrightarrow> t' \<sqsubseteq> t \<Longrightarrow> FV t' = {}" by (induct t) auto

lemma ground_subterm': "FV t = {} \<Longrightarrow> t' \<sqsubset> t \<Longrightarrow> FV t' = {}" by (induct t) auto

lemma ground_subterm'': "FV t = {} \<Longrightarrow> t' \<in> subterms 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_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 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_set_subterms_eq[simp]: "FV\<^sub>s\<^sub>e\<^sub>t M = FV\<^sub>s\<^sub>e\<^sub>t (\<Union>(subterms ` M))"
using subtermeq_vars_subset by force

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> \<Union>(subterms ` M) \<Longrightarrow> FV t \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t M"
using FV_subset FV_set_subterms_eq 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 subset_subterms_Union[simp]: "M \<subseteq> \<Union>(subterms ` M)" by auto

lemma in_subterms_Union: "t \<in> M \<Longrightarrow> t \<in> \<Union>(subterms ` M)" using subset_subterms_Union by blast

lemma in_subterms_subset: "t \<in> subterms t' \<Longrightarrow> subterms t \<subseteq> subterms t'"
by (simp add: subterms_subset)

lemma in_subterms_subset': "M \<subseteq> subterms t \<Longrightarrow> \<Union>(subterms ` M) \<subseteq> subterms t"
by (metis SUP_def SUP_least contra_subsetD in_subterms_subset)

lemma in_subterms_subset_Union: "t \<in> \<Union>(subterms ` M) \<Longrightarrow> subterms t \<subseteq> \<Union>(subterms ` M)"
using subterms_subset by auto

lemma subtermseq_if_subterms: "t' \<sqsubset> t \<Longrightarrow> t' \<sqsubseteq> t" by simp

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 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)+
  thus "s \<sqsubset> Fun f X" "t \<sqsubset> Fun g Y" by blast+
qed

lemma zip_arg_subterm_split:
  assumes "(x,y) \<in> set (zip X Y)"
  obtains X' X'' Y' Y'' where "X = X'@x#X''" "Y = Y'@y#Y''" "length X' = length Y'"
proof -
  from assms have "\<exists>X' X'' Y' Y''. X = X'@x#X'' \<and> Y = Y'@y#Y'' \<and> length X' = length Y'"
  proof (induction Y arbitrary: X)
    case (Cons y' Y' X)
    then obtain x' X' where "X = x'#X'" by (metis empty_iff list.exhaust list.set(1) set_zip_leftD)
    show ?case
    proof (cases "(x, y) \<in> set (zip X' Y')")
      case False
      hence "x = x'" "y = y'" using Cons.prems \<open>X = x'#X'\<close> by auto
      hence "X = []@x#X' \<and> y'#Y' = []@y#Y' \<and> length [] = length []" using \<open>X = x'#X'\<close> by auto
      thus ?thesis by blast
    qed (metis \<open>X = x'#X'\<close> Cons.IH[of X'] Cons_eq_appendI list.size(4))
  qed simp
  thus ?thesis using that by blast
qed

lemma zip_arg_index:
  assumes "(x,y) \<in> set (zip X Y)"
  obtains i where "X ! i = x" "Y ! i = y" "i < length X" "i < length Y"
proof -
  obtain X1 X2 Y1 Y2 where "X = X1@x#X2" "Y = Y1@y#Y2" "length X1 = length Y1"
    using zip_arg_subterm_split[OF assms] by moura
  thus ?thesis using nth_append_length[of X1 x X2] nth_append_length[of Y1 y Y2] that by simp
qed

lemma ground_iff_no_vars: "ground M \<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 simp
  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"
      unfolding ground_def FV\<^sub>s\<^sub>e\<^sub>t_def by blast
    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 (\<Union>t \<in> M. subterms t)"
proof -
  { fix t assume "t \<in> M"
    hence "FV t = {}" using ground_iff_no_vars[of M] \<open>ground M\<close> by simp
    hence "\<forall>t' \<in> subterms t. FV t' = {}" using subtermeq_vars_subset[of _ t] by simp
    hence "ground (subterms t)" by simp
  }
  thus ?thesis by simp
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"
using supteq_imp_funs_term_subset[OF subtermD(2)] by metis

lemma subterms_const: "subterms (Fun f []) = {Fun f []}" by simp

lemma subtermeq_refl[iff]: "t \<sqsubseteq> t" by (induct t rule: subterms.induct) auto

lemma subtermeq_trans[trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" using subterms_subset by auto

lemma subtermeq_antisym:
  assumes "x \<sqsubseteq> y" "y \<sqsubseteq> x"
  shows "x = y"
using assms
proof (induction x arbitrary: y rule: subterms.induct[case_names Var Fun])
  case (Fun f X)
  { assume "y \<noteq> Fun f X"
    then obtain t::"('a,'b) term" where "t \<in> set X" "y \<sqsubseteq> t" using \<open>y \<sqsubseteq> Fun f X\<close> by auto
    hence "Fun f X \<sqsubseteq> t" using subtermeq_trans[OF \<open>Fun f X \<sqsubseteq> y\<close>] by simp
 
    have "t \<sqsubseteq> Fun f X" using \<open>t \<in> set X\<close> by fastforce
    hence "t = Fun f X" using Fun.IH[OF \<open>t \<in> set X\<close> _ \<open>Fun f X \<sqsubseteq> t\<close>] by simp

    have "t \<sqsubseteq> y" using subtermeq_trans[OF \<open>t \<sqsubseteq> Fun f X\<close> \<open>Fun f X \<sqsubseteq> y\<close>] by simp
    hence "t = y" using Fun.IH[OF \<open>t \<in> set X\<close> _ \<open>y \<sqsubseteq> t\<close>] by simp

    have "y = Fun f X" using \<open>t = Fun f X\<close> \<open>t = y\<close> by simp
    hence False using \<open>y \<noteq> Fun f X\<close> by simp
  }
  thus ?case by auto
qed simp

lemma subterms_antisym: "x \<in> subterms y \<Longrightarrow> y \<in> subterms x \<Longrightarrow> x = y"
by (auto simp add: subtermeq_antisym)

lemma subterm_trans[trans]: "x \<sqsubset> y \<Longrightarrow> y \<sqsubset> z \<Longrightarrow> x \<sqsubset> z"
unfolding subterm_def by (meson subtermeq_def subtermeq_trans subterms_antisym)

lemma subterm_irrefl: "\<not>t \<sqsubset> t" by simp

lemma subterm_asym: "t \<sqsubset> u \<Longrightarrow> \<not>u \<sqsubset> t"
using subterm_irrefl subterm_trans by blast

lemma subterm_subtermeq_neq: "\<lbrakk>t \<sqsubset> u; u \<sqsubseteq> v\<rbrakk> \<Longrightarrow> t \<noteq> v"
using subtermeq_antisym by auto

lemma subtermeq_subterm_neq: "\<lbrakk>t \<sqsubseteq> u; u \<sqsubset> v\<rbrakk> \<Longrightarrow> t \<noteq> v"
using subtermeq_antisym by auto

lemma subtermeq_subterm_trans: "\<lbrakk>t \<sqsubseteq> u; u \<sqsubset> v\<rbrakk> \<Longrightarrow> t \<sqsubset> v"
by (metis subtermeqD subterm_trans)

lemma subterm_subtermeq_trans: "\<lbrakk>t \<sqsubset> u; u \<sqsubseteq> v\<rbrakk> \<Longrightarrow> t \<sqsubset> v"
by (metis subtermeqD subterm_trans)

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 subterms_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 subterms_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]: "\<Union>(subterms ` 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_not_in_param: "x \<in> set X \<Longrightarrow> \<not>Fun f X \<sqsubset> x"
using Fun_param_is_subterm[THEN subterm_asym] .

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
      unfolding subterm_def subtermeq_def by auto
  }
  hence "T = []" by (cases T) auto
  thus ?thesis using Fun by simp
qed (simp add: assms)

lemma funs_term_subterms_eq:
  "\<And>t. \<Union>(funs_term ` subterms t) = funs_term t" 
  "\<And>A. \<Union>(funs_term ` (\<Union>(subterms ` A))) = \<Union>(funs_term ` A)"
proof -
  show "\<And>t. \<Union>(funs_term ` subterms t) = funs_term t"
    using in_subterms_refl subtermeq_imp_funs_term_subset unfolding subtermeq_def by blast
  thus "\<And>A. \<Union>(funs_term ` (\<Union>(subterms ` A))) = \<Union>(funs_term ` A)" by force
qed

lemma poss_cons_param: "i <# p \<in> poss t \<Longrightarrow> p \<in> poss (t |_ <i>)"
by (metis append_Empty append_PCons poss_append_poss)

lemma poss_is_subtermeq: assumes "p \<in> poss t" shows "t |_ p \<sqsubseteq> t"
by (fact subtermeq_from_supteq[OF subt_at_imp_supteq[OF assms]])

lemma poss_is_in_subterms: assumes "p \<in> poss t" shows "t |_ p \<in> subterms t"
using poss_is_subtermeq[OF assms] by auto

lemma poss_subtermeq_sup: "p \<in> poss t \<Longrightarrow> s \<sqsubseteq> t |_ p \<Longrightarrow> s \<sqsubseteq> t"
by (metis subterm_def subtermeq_subterm_trans poss_is_subtermeq)

lemma poss_Fun_param: "t \<in> set T \<Longrightarrow> \<exists>i. i < length T \<and> Fun f T |_ <i> = t"
proof (induction T)
  case (Cons t' T) thus ?case by (cases "t = t'") auto
qed auto

end